sup'_eq_of_forall

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.sup'_eq_of_forall

← MathLib Explorer

English

If f(b) = a for all b ∈ s, then s.sup' H f = a.

Русский

Если для всех b ∈ s выполнено f(b) = a, то s.sup' H f = a.

LaTeX

$$$(\forall b \in s, f(b) = a) \Rightarrow s.sup' H f = a$$$

Lean4

theorem sup'_eq_of_forall {a : α} (h : ∀ b ∈ s, f b = a) : s.sup' H f = a :=
  le_antisymm (sup'_le _ _ (fun _ hb ↦ (h _ hb).le)) (le_sup'_of_le _ H.choose_spec (h _ H.choose_spec).ge)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru