mem_full_iff

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

An arrow f from c to d lies in the arrows of the full D iff both its endpoints lie in D.

Русский

Стрела f: c ⟶ d принадлежит стрелкам полной D тогда и только тогда, когда c ∈ D и d ∈ D.

LaTeX

$$$f ∈ (full D).arrows\\ c\\ d \\iff c ∈ D ∧ d ∈ D$$$

Lean4

@[simp]
theorem mem_full_iff {c d : C} {f : c ⟶ d} : f ∈ (full D).arrows c d ↔ c ∈ D ∧ d ∈ D :=
  Iff.rfl

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

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

Разделы

Аффилиация

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