symm — Mathlib

English

If a graph G is bipartite with parts s and t, then it is bipartite with the parts t and s.

Русский

Если граф G двудольен с частями s и t, то он двудольен и с частями t и s.

LaTeX

$$G.IsBipartiteWith s t ⇒ G.IsBipartiteWith t s$$

Lean4

theorem symm (h : G.IsBipartiteWith s t) : G.IsBipartiteWith t s
    where
  disjoint := h.disjoint.symm
  mem_of_adj v w
    hadj := by
    rw [@and_comm (v ∈ t) (w ∈ s), @and_comm (v ∈ s) (w ∈ t)]
    exact h.mem_of_adj hadj.symm

Похожие утверждения