mem_facets — Mathlib

English

A finite face s belongs to the facets of K if and only if s is a face of K and s is maximal among faces (no strictly larger face contains s).

Русский

Грань s принадлежит фасетам K тогда и только тогда, когда s является гранью K и максимальна среди граней (нет строго большего множества, включающего s).

LaTeX

$$$s \\in K.facets \\iff s \\in K.faces \\land (\\forall t ∈ K.faces,\; s ⊆ t \\Rightarrow s = t)$$$

Lean4

theorem mem_facets : s ∈ K.facets ↔ s ∈ K.faces ∧ ∀ t ∈ K.faces, s ⊆ t → s = t :=
  mem_sep_iff

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