binary_relation_sInf_iff — Mathlib

English

Let S be a set of binary predicates r: α × β → Prop. The infimum of S evaluated at (a,b) holds exactly when for every r ∈ S, r(a,b) is true.

Русский

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

LaTeX

$$$sInf s a b \leftrightarrow \forall r : \alpha \to \beta \to Prop,\, r \in s \to r(a,b)$$$

Lean4

theorem binary_relation_sInf_iff {α β : Type*} (s : Set (α → β → Prop)) {a : α} {b : β} :
    sInf s a b ↔ ∀ r : α → β → Prop, r ∈ s → r a b := by simp

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