restrictSurjective_of_add_le_natCard

English

Let α be a finite, s ⊆ α, and hn : s.ncard + n ≤ Nat.card α. Then ∃ y : Fin n ↪ α with Disjoint s and range y.

Русский

Пусть α конечна, s ⊆ α, и s.ncard + n ≤ Nat.card α. Тогда ∃ вложение y: Fin n ↪ α, такое что Disjoint s и range y.

LaTeX

$$[Finite α] \\land s.ncard + n ≤ Nat.card α \\Rightarrow ∃ y : Fin n ↪ α, Disjoint s (range y).$$

Lean4

theorem restrictSurjective_of_add_le_natCard [Finite α] (hn : m + n ≤ Nat.card α) :
    Surjective (fun x : Fin (m + n) ↪ α ↦ (castAddEmb n).trans x) :=
  by
  apply restrictSurjective_of_add_le_ENatCard
  rwa [← ENat.coe_add, ENat.card_eq_coe_natCard, ENat.coe_le_coe]

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