Icc_bot_top — Mathlib

English

If α is a preorder with both a bottom and a top element, the closed interval [⊥, ⊤] contains all elements of α.

Русский

Пусть α — предзаказ с нижней и верхней границей; закрытый интервал [⊥, ⊤] содержит все элементы α.

LaTeX

$$$\{ x \in \alpha \mid \bot \le x \le \top \} = \alpha$$$

Lean4

theorem Icc_bot_top [Preorder α] [BoundedOrder α] : Icc (⊥ : α) ⊤ = univ := by simp

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