exists_bijOn_of_map — Mathlib

English

For an injected-on ground mapping, if I is independent in M.map f hf, there exists I0 with M.Indep I0 and BijOn f I0 I.

Русский

При отображении с вложением, если I независимо в M.map f hf, существует I0 с M.Indep I0 и BijOn f I0 I.

LaTeX

$$$\exists I_0,\ M.Indep I_0 \land \mathrm{BijOn} f I_0 I$$$

Lean4

theorem exists_bijOn_of_map {I : Set β} (hf) (hI : (M.map f hf).Indep I) : ∃ I₀, M.Indep I₀ ∧ BijOn f I₀ I :=
  by
  obtain ⟨I₀, hI₀, rfl⟩ := hI
  exact ⟨I₀, hI₀, (hf.mono hI₀.subset_ground).bijOn_image⟩

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