completeEquipartiteGraph_eq_bot_iff

English

An equal-edges complete equipartite graph has no edges exactly when r ≤ 1 or t = 0.

Русский

Граф K_r(t) пустого типа имеет ребра отсутствуют тогда и только тогда, когда r ≤ 1 или t = 0.

LaTeX

$$completeEquipartiteGraph r t = ⊥ ↔ r ≤ 1 ∨ t = 0$$

Lean4

/-- `completeEquipartiteGraph r t` contains no edges when `r ≤ 1` or `t = 0`. -/
theorem completeEquipartiteGraph_eq_bot_iff : completeEquipartiteGraph r t = ⊥ ↔ r ≤ 1 ∨ t = 0 :=
  by
  rw [← not_iff_not, not_or, ← ne_eq, ← edgeSet_nonempty, not_le, ← Nat.succ_le_iff, ← Fin.nontrivial_iff_two_le, ←
    ne_eq, ← Nat.pos_iff_ne_zero, Fin.pos_iff_nonempty]
  refine ⟨fun ⟨e, he⟩ ↦ ?_, fun ⟨⟨i₁, i₂, hv⟩, ⟨x⟩⟩ ↦ ?_⟩
  · induction e with
    | _ v₁ v₂
    rw [mem_edgeSet, completeEquipartiteGraph_adj] at he
    exact ⟨⟨v₁.1, v₂.1, he⟩, ⟨v₁.2⟩⟩
  · use s((i₁, x), (i₂, x))
    rw [mem_edgeSet, completeEquipartiteGraph_adj]
    exact hv

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