bot_isContained_iff_card_le — Mathlib

English

(⊥ : SimpleGraph α) ⊑ B iff card α ≤ card β (for finite α, β).

Русский

Нижний граф ⊥ содержится в B тогда и только тогда, когда число вершин α не превосходит число вершин β.

LaTeX

$$(⊥ : SimpleGraph α) ⊑ B ↔ Fintype.card α ≤ Fintype.card β$$

Lean4

/-- `⊥` is contained in any simple graph having sufficiently many vertices. -/
theorem bot_isContained_iff_card_le [Fintype α] [Fintype β] :
    (⊥ : SimpleGraph α) ⊑ B ↔ Fintype.card α ≤ Fintype.card β :=
  ⟨fun ⟨f⟩ ↦ Fintype.card_le_of_embedding f.toEmbedding, fun h ↦
    ⟨Copy.bot (Function.Embedding.nonempty_of_card_le h).some⟩⟩

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