comapOn_isBase_iff_of_bijOn — Mathlib

English

If f is bijective between B and its image within E, then (N.comapOn E f).IsBase B is equivalent to N.IsBase (f''B) ∧ B ⊆ E.

Русский

Если f биективно ограничивает B и его образ в E, то (N.comapOn E f).IsBase B эквивалентно N.IsBase (f''B) ∧ B ⊆ E.

LaTeX

$$$ (N.comapOn E f).IsBase B \iff N.IsBase (f''B) \land B \subseteq E $$$

Lean4

theorem comapOn_isBase_iff_of_bijOn (h : BijOn f E N.E) : (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ B ⊆ E :=
  by
  rw [← and_iff_left_of_imp (IsBase.subset_ground (M := N.comapOn E f) (B := B)), comapOn_ground_eq, and_congr_left_iff]
  suffices h' : B ⊆ E → InjOn f B from fun hB ↦ by simp [hB, comapOn_isBase_iff_of_surjOn h.surjOn, h']
  exact fun hBE ↦ h.injOn.mono hBE

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