unary_relation_sSup_iff — Mathlib

English

For any set s of predicates on α, the supremum at a is equivalent to the existence of a predicate in s that holds at a.

Русский

Для любого множества предикатов на α верхняя грань в точке a эквивалентна существованию предиката p ∈ s, который истинен в a.

LaTeX

$$$\\displaystyle sSup\\,s\\,a \\;\\Longleftrightarrow\\; \\exists r:\\alpha\\to\\mathrm{Prop},\\ r\\in s \\land r(a)$$$

Lean4

theorem unary_relation_sSup_iff {α : Type*} (s : Set (α → Prop)) {a : α} : sSup s a ↔ ∃ r : α → Prop, r ∈ s ∧ r a := by
  simp

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