nonempty_iInter_Iic_iff — Mathlib

English

In a Preorder, the nonempty intersection of all downward closed sets Iic(f(i)) is equivalent to the existence of a global lower bound for the range of f.

Русский

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

LaTeX

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

Lean4

theorem nonempty_iInter_Iic_iff [Preorder α] {f : ι → α} : (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f) :=
  by
  have : (⋂ (i : ι), Iic (f i)) = lowerBounds (range f) := by ext c; simp [lowerBounds]
  simp [this, BddBelow]

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