| Popis: |
Za namene formalizacije ravninskih grafov v dokazovalniku Lean uvedemo matematični pojem kombinatoričnih preslikav in zanj predstavimo karakterizacijo ravninskih grafov, za katero dokažemo tudi smiselnost. Pojem kombinatoričnih preslikav v dokazovalniku Lean formaliziramo na način, ki omogoča lastnosti, s katerimi lahko neposredno računamo. Formaliziramo dokaz, da so tako podane kombinatorične preslikave skladne z njihovo matematično definicijo. For the purposes of formalizing planar graphs in the proof assistant Lean, we define combinatorial maps and show how they characterize planar graphs, where we also prove the correctness of the characterization. Using Lean we formalize combinatorial maps in such a way, that their properties can be computed. Finally we show that the given formalization of combinatorial maps corresponds to the mathematical definition of combinatorial maps. |
