inv_mem_iff — Mathlib

English

For a morphism f in a Groupoid-subgroupoid S, inv f ∈ S.arrows d c if and only if f ∈ S.arrows c d.

Русский

Для морфизма f ∈ S.arrows c d верно: inv f ∈ S.arrows d c тогда и только тогда, когда f ∈ S.arrows c d.

LaTeX

$$$\\text{inv}\\; f \\in S.arrows\\ d\\ c \\iff f \\in S.arrows\\ c\\ d$$$

Lean4

theorem inv_mem_iff {c d : C} (f : c ⟶ d) : Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d :=
  by
  constructor
  · intro h
    simpa only [inv_eq_inv, IsIso.inv_inv] using S.inv h
  · apply S.inv

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