isTotallyDisconnected_iff — Mathlib

English

A Subgroupoid S of a groupoid C is totally disconnected if and only if whenever there exists a morphism in S from c to d, then c = d.

Русский

Подгруппоида S группы C полностью разобщённа тогда и только тогда, когда существование морфизма из c в d в S влечёт равенство объектов c = d.

LaTeX

$$$S.IsTotallyDisconnected \\iff \\forall c d : C,\\ (S.arrows\\ c d).Nonempty \\rightarrow c = d$$$

Lean4

theorem isTotallyDisconnected_iff : S.IsTotallyDisconnected ↔ ∀ c d, (S.arrows c d).Nonempty → c = d :=
  by
  constructor
  · rintro h c d ⟨f, fS⟩
    exact congr_arg Subtype.val <| h ⟨c, mem_objs_of_src S fS⟩ ⟨d, mem_objs_of_tgt S fS⟩ ⟨f, fS⟩
  · rintro h ⟨c, hc⟩ ⟨d, hd⟩ ⟨f, fS⟩
    simp only [Subtype.mk_eq_mk]
    exact h c d ⟨f, fS⟩

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