mono — Mathlib

English

If G ≤ H and H is clique-free on s, then G is clique-free on s as well (anti-monotonicity).

Русский

Если G ⊆ H и H не содержит n-клик на s, то G тоже не содержит (n)-клик на s.

LaTeX

$$If $G \le H$ and $H$ is $n$-clique-free on $s$, then $G$ is $n$-clique-free on $s$.$$

Lean4

theorem mono (hmn : m ≤ n) (hG : G.CliqueFreeOn s m) : G.CliqueFreeOn s n :=
  by
  rintro t hts ht
  obtain ⟨u, hut, hu⟩ := exists_subset_card_eq (hmn.trans ht.card_eq.ge)
  exact hG ((coe_subset.2 hut).trans hts) ⟨ht.isClique.subset hut, hu⟩

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