isCompleteMultipartite — Mathlib

English

The complete equipartite graph K_r(t) is complete multipartite.

Русский

Полный равновесный граф K_r(t) является полным мультитипным графом.

LaTeX

$$(completeEquipartiteGraph r t).IsCompleteMultipartite$$

Lean4

theorem isCompleteMultipartite : (completeEquipartiteGraph r t).IsCompleteMultipartite :=
  by
  rcases t.eq_zero_or_pos with ht_eq0 | ht_pos
  · rw [completeEquipartiteGraph_eq_bot_iff.mpr (Or.inr ht_eq0)]
    exact bot_isCompleteMultipartite
  · rw [isCompleteMultipartite_iff]
    use (Fin r), Function.const (Fin r) (Fin t)
    simp_rw [Function.const_apply, exists_prop]
    exact
      ⟨Function.const (Fin r) (Fin.pos_iff_nonempty.mp ht_pos), ⟨completeEquipartiteGraph.completeMultipartiteGraph⟩⟩

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