instSemilatticeInf — Mathlib

English

Re-states that x ∈ K.vertices iff {x} ∈ K.faces.

Русский

Повторяет, что x принадлежит вершинам K тогда и только тогда, когда {x} является гранью K.

LaTeX

$$x ∈ K.vertices ↔ {x} ∈ K.faces$$

Lean4

instance : SemilatticeInf (SimplicialComplex 𝕜 E) :=
  {
    PartialOrder.lift faces (fun _ _ =>
        SimplicialComplex.ext) with
    inf := (· ⊓ ·)
    inf_le_left := fun _ _ _ hs => hs.1
    inf_le_right := fun _ _ _ hs => hs.2
    le_inf := fun _ _ _ hKL hKM _ hs => ⟨hKL hs, hKM hs⟩ }

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