cliqueFree_map_iff — Mathlib

English

There exists a top embedding witnessing not_cliqueFree; i.e., a witness that there is a copy of a finite complete graph inside G.

Русский

Существует верхнее вложение, подтверждающее неclique-free; то есть копия полного графа внутри G.

LaTeX

$$$ \exists f : (\top : SimpleGraph( Fin n)) \hookrightarrow G. $$$

Lean4

@[simp]
theorem cliqueFree_map_iff {f : α ↪ β} [Nonempty α] : (G.map f).CliqueFree n ↔ G.CliqueFree n :=
  by
  obtain (hle | hlt) := le_or_gt n 1
  · obtain (rfl | rfl) := Nat.le_one_iff_eq_zero_or_eq_one.1 hle
    · simp [CliqueFree]
    simp [CliqueFree, show ∃ (_ : β), True from ⟨f (Classical.arbitrary _), trivial⟩]
  simp [CliqueFree, isNClique_map_iff hlt]

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