instCompleteSemilatticeInf — Mathlib

English

The structure of nuclei forms a complete semilattice with Inf as the infimum operation.

Русский

Структура нуклеусов образует полную частичную упорядоченную структуру с Inf как операцией инфимума.

LaTeX

$$$\text{CompleteSemilatticeInf}(Nucleus(X))$$$

Lean4

instance : CompleteSemilatticeInf (Nucleus X)
    where
  sInf_le := by simp +contextual [← coe_le_coe, Pi.le_def, iInf_le_iff]
  le_sInf := by simp +contextual [← coe_le_coe, Pi.le_def]

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