Ici_eq — Mathlib

English

If a is the bottom element, then the interval Ici a equals the entire universe; i.e., every x ≥ a holds for all x.

Русский

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

LaTeX

$$$$ \text{IsBot}(a) \implies Ici a = \text{univ} $$$$

Lean4

theorem _root_.IsBot.Ici_eq (h : IsBot a) : Ici a = univ :=
  eq_univ_of_forall h

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