exists_embedding_disjoint_range_of_add_le_Nat_card

English

Let α be finite. If s.ncard + n ≤ Nat.card α, then ∃ y : Fin n ↪ α, Disjoint s (range y).

Русский

Пусть α конечна. Если s.ncard + n ≤ Nat.card α, существует вложение y: Fin n ↪ α с Disjoint s (range y).

LaTeX

$$$s.ncard + n \\le Nat.card \\alpha \\Rightarrow \\exists y : Fin(n) \\hookrightarrow \\alpha, \\operatorname{Disjoint}(s, \\operatorname{range}(y)).$$$

Lean4

theorem exists_embedding_disjoint_range_of_add_le_Nat_card [Finite α] (hs : s.ncard + n ≤ Nat.card α) :
    ∃ y : Fin n ↪ α, Disjoint s (range y) :=
  by
  apply exists_embedding_disjoint_range_of_add_le_ENat_card
  rwa [← ENat.coe_add, ENat.card_eq_coe_natCard, ENat.coe_le_coe]

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