mem_sInf_arrows — Mathlib

English

An arrow p lies in the arrows of the infimum of a family s of subgroupoids exactly when p lies in the arrows of every member of s.

Русский

Стрела p принадлежит стрелам дуального пересечения множеств подгруппоиодов тогда, когда она принадлежит стрелам каждого элемента множества s.

LaTeX

$$p ∈ (sInf s).arrows c d ↔ ∀ S ∈ s, p ∈ S.arrows c d$$

Lean4

theorem mem_sInf_arrows {s : Set (Subgroupoid C)} {c d : C} {p : c ⟶ d} :
    p ∈ (sInf s).arrows c d ↔ ∀ S ∈ s, p ∈ S.arrows c d :=
  mem_iInter₂

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