restrictSurjective_of_le_ENatCard

English

If m ≤ n and n ≤ ENat.card α, then the map x ↦ (castLEEmb hmn).trans x is surjective from Fin n ↪ α to Fin m ↪ α.

Русский

Если m ≤ n и n ≤ ENat.card α, отображение x ↦ (castLEEmb hmn).trans x сюръективно из Fin n ↪ α на Fin m ↪ α.

LaTeX

$$$m \\le n \\land n \\le ENat.card \\alpha \\Rightarrow \\operatorname{Surjective}\\left(\\lambda x : Fin n \\hookrightarrow \\alpha, (castLEEmb hmn).trans x\\right).$$$

Lean4

theorem restrictSurjective_of_le_ENatCard (hmn : m ≤ n) (hn : n ≤ ENat.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_ENatCard hn

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