Iic_eq — Mathlib

English

If a is a top element, then the interval Iic a equals the entire universe; i.e., every x ≤ a holds for all x.

Русский

Если a — максимальный элемент, то интервал Iic a равен всему множеству; то есть каждый элемент удовлетворяет x ≤ a.

LaTeX

$$$$ \text{IsTop}(a) \implies Iic a = \text{univ} $$$$

Lean4

theorem _root_.IsTop.Iic_eq (h : IsTop a) : Iic a = univ :=
  eq_univ_of_forall h

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