le_sSupFun

Mathlib.Algebra.Order.Module.HahnEmbedding

URI: https://scilib.ai/kg/mathlib#HahnEmbedding.Partial.le_sSupFun

← MathLib Explorer

English

If f belongs to a directed set c, then f.val ≤ sSupFun hc.

Русский

Если f принадлежит направленному множеству c, тогда f.val ≤ sSupFun hc.

LaTeX

$$hf: f ∈ c ⇒ f.val ≤ sSupFun hc$$

Lean4

theorem le_sSupFun {c : Set (Partial seed)} (hc : DirectedOn (· ≤ ·) c) {f : Partial seed} (hf : f ∈ c) :
    f.val ≤ sSupFun hc :=
  LinearPMap.le_sSup _ <| (Set.mem_image _ _ _).mpr ⟨f, hf, rfl⟩

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

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

Разделы

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

Аффилиация

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