mem_sInf

Mathlib.CategoryTheory.Groupoid.Subgroupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subgroupoid.mem_sInf

English

An element p lies in sInf s precisely if p belongs to every S ∈ s.

Русский

Элемент p принадлежит sInf s тогда и только тогда, когда он принадлежит каждому S ∈ s.

LaTeX

$$p ∈ sInf s ↔ ∀ S ∈ s, p ∈ S$$

Lean4

theorem mem_sInf {s : Set (Subgroupoid C)} {p : Σ c d : C, c ⟶ d} : p ∈ sInf s ↔ ∀ S ∈ s, p ∈ S :=
  mem_sInf_arrows

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru