English
There exists a flat F with F ⊆ M.E and containing X ∩ M.E.
Русский
Существует плоское множество F такое, что F ⊆ M.E и содержит X ∩ M.E.
LaTeX
$$$\exists F, M.IsFlat F ∧ (X \cap M.E) \subseteq F$$$
Lean4
/-- The property of being a flat gives rise to a `ClosureOperator` on the subsets of `M.E`,
in which the `IsClosed` sets correspond to flats.
(We can't define such an operator on all of `Set α`,
since this would incorrectly force `univ` to always be a flat.) -/
def subtypeClosure (M : Matroid α) : ClosureOperator (Iic M.E) :=
ClosureOperator.ofCompletePred (fun F ↦ M.IsFlat F.1) fun s hs ↦
by
obtain (rfl | hne) := s.eq_empty_or_nonempty
· simp
have _ := hne.coe_sort
convert IsFlat.iInter (M := M) (Fs := fun (F : s) ↦ F.1.1) (fun F ↦ hs F.1 F.2)
ext
aesop
