mem_disconnect_objs_iff — Mathlib

English

For any subgroupoid S, c belongs to the disconnect objects iff c belongs to S objects.

Русский

Для подгруппоида S выполняется: c входит в области объектов S.disconnect тогда и только тогда, когда входит в области объектов S.

LaTeX

$$$\\forall {c : C}, c \\in S.disconnect.objs \\iff c \\in S.objs$$$

Lean4

@[simp]
theorem mem_disconnect_objs_iff {c : C} : c ∈ S.disconnect.objs ↔ c ∈ S.objs :=
  ⟨fun ⟨γ, _, γS⟩ => ⟨γ, γS⟩, fun ⟨γ, γS⟩ => ⟨γ, rfl, γS⟩⟩

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