closure — Mathlib

English

A set F is flat if and only if its closure equals itself.

Русский

Множество F плоско тогда и только тогда, когда его замыкание равно самому F.

LaTeX

$$$M.IsFlat F \iff M.closure F = F$$$

Lean4

/-- The closure of `X ⊆ M.E` is the intersection of all the flats of `M` containing `X`.
A set `X` that doesn't satisfy `X ⊆ M.E` has the junk value `M.closure X := M.closure (X ∩ M.E)`. -/
def closure (M : Matroid α) (X : Set α) : Set α :=
  ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}

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