isFlat_iff_isClosed — Mathlib

English

The subtype-closure defined from flats on the ground equals the closure induced by the ambient matroid on the subtype. (Equivalence of two closure notions on the ground set.)

Русский

Область замыкания, определяемая через подмножество, совпадает с замыканием, полученным из матроида на подмножество. (Эквивалентность двух определений замыкания на основании основания).

LaTeX

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

Lean4

theorem isFlat_iff_isClosed : M.IsFlat F ↔ ∃ h : F ⊆ M.E, M.subtypeClosure.IsClosed ⟨F, h⟩ := by
  simpa [subtypeClosure] using IsFlat.subset_ground

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