closure_diff_ssubset — Mathlib

English

If I is independent and (I ∩ X) is nonempty, then M.closure(I \\ X) ⊊ M.closure(I).

Русский

Если I независимо, и I ∩ X непусто, то closure(I \\ X) ⊊ closure(I).

LaTeX

$$$ \\text{If } hI : M.Indep I \\text{ and } (I \\cap X).Nonempty, \\; M.\\mathrm{closure}(I \\setminus X) \\subset M.\\mathrm{closure}(I) $$$

Lean4

theorem closure_diff_ssubset (hI : M.Indep I) (hX : (I ∩ X).Nonempty) : M.closure (I \ X) ⊂ M.closure I :=
  by
  refine hI.closure_ssubset_closure <| diff_subset.ssubset_of_ne fun h ↦ ?_
  rw [sdiff_eq_left, disjoint_iff_inter_eq_empty] at h
  simp [h] at hX

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