sInf_iff — Mathlib

English

For S a set of Setoids on α, the relation sInf S relates x and y exactly when every s ∈ S relates x and y.

Русский

Для множества S отношений эквивалентности на α, отношение sInf S оказывает связь x и y тогда, когда для каждого s ∈ S выполняется s x y.

LaTeX

$$$$ sInf S\\ x\\ y \\iff \\forall s \\in S,\\ s.r\\ x\\ y. $$$$

Lean4

theorem sInf_iff {S : Set (Setoid α)} {x y : α} : sInf S x y ↔ ∀ s ∈ S, s x y :=
  Iff.rfl

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