exists_eq_iSup_of_lt_top — Mathlib

English

Let ι be nonempty. If h : ⨆ i, f i < ⊤, then ∃ i, f i = ⨆ i, f i.

Русский

Пусть ι непусто. Если h : ⨆ i, f i < ⊤, то найдётся i такое, что f i = ⨆ i, f i.

LaTeX

$$$[Nonempty \iota] \; (h : \bigl(\bigvee_i f(i)\bigr) < \top) \Rightarrow \exists i, f(i) = \bigl(\bigvee_i f(i)\bigr)$$$

Lean4

theorem exists_eq_iSup_of_lt_top [Nonempty ι] (h : ⨆ i, f i < ⊤) : ∃ i, f i = ⨆ i, f i :=
  sSup_mem_of_nonempty_of_lt_top h

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