closure_eq_subtypeClosure — Mathlib

English

The closure of X equals the subtypeClosure of ⟨X ∩ M.E, proof⟩.

Русский

Замыкание X равно подтиповому замыканию ⟨X ∩ M.E, доказательство⟩.

LaTeX

$$$M.closure X = M.subtypeClosure \langle X \cap M.E, \text{inter_subset_right} \rangle$$$

Lean4

theorem closure_eq_subtypeClosure (M : Matroid α) (X : Set α) :
    M.closure X = M.subtypeClosure ⟨X ∩ M.E, inter_subset_right⟩ :=
  by
  suffices
    ∀ (x : α),
      (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ (x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a)
    by simpa [closure, subtypeClosure, Set.ext_iff]
  exact fun x ↦
    ⟨fun h ↦ ⟨h _ M.ground_isFlat inter_subset_right, fun F _ hXF hF ↦ h F hF hXF⟩, fun ⟨_, h⟩ F hF hXF ↦
      h F hF.subset_ground hXF hF⟩

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