toBoundedOrder — Mathlib

English

A Heyting algebra automatically carries a bounded order structure, i.e., there exists a bottom element ⊥ with ⊥ ≤ x for all x.

Русский

Хейтингова алгебра автоматически образует ограниченный порядок, то есть существует нижний элемент ⊥, такой что ⊥ ≤ x для всякого x.

LaTeX

$$$ \forall x\, (x\in \alpha),\ \bot \le x $$$

Lean4

instance (priority := 100) toBoundedOrder [HeytingAlgebra α] : BoundedOrder α :=
  { bot_le := ‹HeytingAlgebra α›.bot_le }
    -- See note [lower instance priority]

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