unary_relation_sInf_iff — Mathlib

English

Let S be a set of predicates r: α → Prop. For a fixed a ∈ α, the infimum over S evaluated at a equals the conjunction of all r(a) with r ∈ S; equivalently, a satisfies every predicate in S exactly when sInf S a holds.

Русский

Пусть S — множество предикатов r: α → Prop. Для фиксированного a ∈ α инфимум множества S, применённый к a, равен конъюнкции всех r(a) с r ∈ S; то есть a удовлетворяет каждому предикату из S тогда и только тогда, когда sInf S a истинно.

LaTeX

$$$sInf s a \leftrightarrow \forall r : \alpha \to \mathrm{Prop},\, r \in s \to r a$$$

Lean4

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

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