InfClosed — Mathlib

English

A set s is inf-closed if it contains the infimum a ⊓ b whenever a,b ∈ s.

Русский

Множество s инф-замкнуто, если для любых a,b ∈ s их infimum a ⊓ b принадлежит s.

LaTeX

$$$ \\text{InfClosed}(s) \\;:=\\; \\forall a \\in s, \\forall b \\in s, a \\wedge b \\in s$$$

Lean4

/-- A set `s` is *inf-closed* if `a ⊓ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/
def InfClosed (s : Set α) : Prop :=
  ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ⊓ b ∈ s

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