sup'_lt_iff — Mathlib

English

Let s be nonempty finite subset of α and f: ι → α. Then s.sup' H f < a iff ∀ i ∈ s, f(i) < a.

Русский

Пусть s непустое конечное подмножество и f: ι → α. Тогда sup' над s меньше a тогда и только тогда, когда для всех i ∈ s выполняется f(i) < a.

LaTeX

$$$s.sup' H f < a \iff \forall i \in s, f(i) < a.$$$

Lean4

@[simp]
theorem sup'_lt_iff : s.sup' H f < a ↔ ∀ i ∈ s, f i < a :=
  by
  rw [← WithBot.coe_lt_coe, coe_sup', Finset.sup_lt_iff (WithBot.bot_lt_coe a)]
  exact forall₂_congr (fun _ _ => WithBot.coe_lt_coe)

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