instMin — Mathlib

English

The complex obtained by intersecting the face-sets of two complexes K and L has faces K.faces ∩ L.faces, and the other data are inherited.

Русский

Комплекс, получаемый пересечением множеств граней двух комплексов K и L, имеет грани K.faces ∩ L.faces и остальные данные наследуются.

LaTeX

$$faces(K) ∩ faces(L) = faces(K ⊓ L)$$

Lean4

/-- The complex consisting of only the faces present in both of its arguments. -/
instance : Min (SimplicialComplex 𝕜 E) :=
  ⟨fun K L =>
    { faces := K.faces ∩ L.faces
      empty_notMem := fun h => K.empty_notMem (Set.inter_subset_left h)
      indep := fun hs => K.indep hs.1
      down_closed := fun hs hst ht => ⟨K.down_closed hs.1 hst ht, L.down_closed hs.2 hst ht⟩
      inter_subset_convexHull := fun hs ht => K.inter_subset_convexHull hs.1 ht.1 }⟩

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