le_iff — Mathlib

English

The subgroupoid order is defined by inclusion of arrows: S ≤ T if and only if for all c,d, S.arrows(c,d) ⊆ T.arrows(c,d).

Русский

Порядок подгрупподиодов задаётся включением стрел: S ≤ T тогда и только тогда, когда для всех c,d выполняется S.arrows(c,d) ⊆ T.arrows(c,d).

LaTeX

$$S ≤ T ↔ ∀ {c d}, S.arrows c d ⊆ T.arrows c d.$$

Lean4

theorem le_iff (S T : Subgroupoid C) : S ≤ T ↔ ∀ {c d}, S.arrows c d ⊆ T.arrows c d := by
  rw [SetLike.le_def, Sigma.forall]; exact forall_congr' fun c => Sigma.forall

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