closure_ssubset_closure — Mathlib

English

If I is independent and J ⊂ I, then closure(J) is strictly contained in closure(I).

Русский

Если I — независимое множество и J ⊂ I, то closure(J) ⊊ closure(I).

LaTeX

$$$ \\text{If } hI : M.Indep I \\text{ and } hJI : J \\subset I, \\; M.\\mathrm{closure}(J) \\;\\subset\\; M.\\mathrm{closure}(I) $$$

Lean4

theorem closure_ssubset_closure (hI : M.Indep I) (hJI : J ⊂ I) : M.closure J ⊂ M.closure I :=
  by
  obtain ⟨e, heI, heJ⟩ := exists_of_ssubset hJI
  exact
    (M.closure_subset_closure hJI.subset).ssubset_of_not_subset fun hss ↦
      heJ <| (hI.closure_inter_eq_self_of_subset hJI.subset).subset ⟨hss (M.mem_closure_of_mem heI), heI⟩

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