binary_relation_sSup_iff — Mathlib

English

Let S be a set of binary predicates r: α × β → Prop. The supremum of S evaluated at (a,b) holds exactly when there exists a predicate r ∈ S such that r(a,b) is true.

Русский

Пусть S — множество двоичных предикатов r: α × β → Prop. Верхняя грань множества S, применённая к паре (a,b), истинна тогда и только если существует r ∈ S такое, что r(a,b) истинно.

LaTeX

$$$sSup s a b \leftrightarrow \exists r : \alpha \to \beta \to Prop,\, r \in s \land r(a,b)$$$

Lean4

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

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