isBasis'_iff_isBasis_closure — Mathlib

English

For all α, I, X, M.IsBasis′ I X iff M.IsBasis I (closure X) ∧ I ⊆ X.

Русский

Для всех α, I, X: M.IsBasis′ I X эквивалентно M.IsBasis I (замыкание X) и I ⊆ X.

LaTeX

$$$M.IsBasis' I X \iff M.IsBasis I (M.closure X) \land I \subseteq X$$$

Lean4

theorem isBasis'_iff_isBasis_closure : M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X :=
  by
  rw [← closure_inter_ground, isBasis'_iff_isBasis_inter_ground]
  exact
    ⟨fun h ↦ ⟨h.isBasis_closure_right, h.subset.trans inter_subset_left⟩, fun h ↦
      h.1.isBasis_subset (subset_inter h.2 h.1.indep.subset_ground) (M.subset_closure _)⟩

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