restrictSurjective_of_le_natCard — Mathlib

English

Let α be finite. If hmn: m ≤ n and hn: n ≤ Nat.card α, then map x ↦ (castLEEmb hmn).trans x is surjective.

Русский

Пусть α конечна. Если m ≤ n и n ≤ Nat.card α, тогда отображение x ↦ (castLEEmb hmn).trans x сюръективно.

LaTeX

$$$[Finite \\alpha] \\; (hmn : m \\le n) (hn : n \\le Nat.card \\alpha) \\rightarrow \\operatorname{Surjective} (\\lambda x : Fin n \\hookrightarrow \\alpha, \\; (castLEEmb hmn).trans x).$$$

Lean4

theorem restrictSurjective_of_le_natCard [Finite α] (hmn : m ≤ n) (hn : n ≤ Nat.card α) :
    Function.Surjective (fun x : Fin n ↪ α ↦ (castLEEmb hmn).trans x) :=
  by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  exact Fin.Embedding.restrictSurjective_of_add_le_natCard hn

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