turanGraph_eq_top — Mathlib

English

The Turán graph is top (i.e., equals the universal complete graph) if and only if r = 0 or n ≤ r.

Русский

Граф Турэна равен топу тогда, когда r = 0 или n ≤ r.

LaTeX

$$$turanGraph(n,r) = \top \iff r = 0 \lor n \le r$.$$

Lean4

@[simp]
theorem turanGraph_eq_top : turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r :=
  by
  simp_rw [SimpleGraph.ext_iff, funext_iff, turanGraph, top_adj, eq_iff_iff, not_iff_not]
  refine ⟨fun h ↦ ?_, ?_⟩
  · contrapose! h
    use ⟨0, (Nat.pos_of_ne_zero h.1).trans h.2⟩, ⟨r, h.2⟩
    simp [h.1.symm]
  · rintro (rfl | h) a b
    · simp [Fin.val_inj]
    · rw [Nat.mod_eq_of_lt (a.2.trans_le h), Nat.mod_eq_of_lt (b.2.trans_le h), Fin.val_inj]

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