comapOn_isBase_iff_of_surjOn — Mathlib

English

If f is surjective on E with respect to N.E, then the IsBase criterion simplifies: (N.comapOn E f).IsBase B iff (N.IsBase (f''B) ∧ InjOn f B ∧ B ⊆ E).

Русский

Если отображение f сюръектно на E относительно N.E, то критерий IsBase упрощается: (N.comapOn E f).IsBase B эквивалентно N.IsBase (f(B)) ∧ InjOn f B ∧ B ⊆ E.

LaTeX

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

Lean4

theorem comapOn_isBase_iff_of_surjOn (h : SurjOn f E N.E) :
    (N.comapOn E f).IsBase B ↔ (N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E) := by
  simp_rw [comapOn_isBase_iff, and_congr_left_iff, and_imp, isBasis'_iff_isBasis_inter_ground,
    inter_eq_self_of_subset_right h, isBasis_ground_iff, implies_true]

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