sInf_equiv — Mathlib

English

Let S be a set of equivalence relations on α. The infimum (greatest lower bound) of S is the relation x ~ y if and only if x ~_s y for every s ∈ S.

Русский

Пусть S — множество отношений эквивалентности на α. Инфимума S есть отношение, при котором x эквивалентно y тогда и только тогда, когда x эквивалентно y во всех отношениях s ∈ S.

LaTeX

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

Lean4

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

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