nonempty_iInter_Ici_iff — Mathlib

English

In a Preorder with dual ordering, the nonempty intersection of all Ici(f(i)) is equivalent to the existence of an upper bound for the range of f.

Русский

В предерассмотре (с тёмной двойственной упорядоченностью) непустое пересечение Ici(f(i)) эквивалентно существованию верхней границы для {f(i)}.

LaTeX

$$$$ (\\bigcap_i Ici(f(i))).Nonempty \\iff \\exists a, \\forall i, f(i) \\le a. $$$$

Lean4

theorem nonempty_iInter_Ici_iff [Preorder α] {f : ι → α} : (⋂ i, Ici (f i)).Nonempty ↔ BddAbove (range f) :=
  nonempty_iInter_Iic_iff (α := αᵒᵈ)

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