closure_eq_of_superset — Mathlib

English

If S is spanning and S ⊆ T, then the closure of T is the ground set E.

Русский

Если S является образующим множество и S ⊆ T, то замыкание T равно множеству E.

LaTeX

$$$$ M.\mathrm{closure}(T) = M.E \\text{ whenever } M.Spanning(S) \text{ and } S \subseteq T. $$$$

Lean4

theorem closure_eq_of_superset (hS : M.Spanning S) (hST : S ⊆ T) : M.closure T = M.E :=
  by
  rw [← closure_inter_ground, ← spanning_iff_closure_eq]
  exact hS.superset (subset_inter hST hS.subset_ground)

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