mem_groupoid_of_pregroupoid — Mathlib

English

Membership equivalence: an element belongs to the groupoid iff the pair (e, source/target) satisfies the pregrouppoid property.

Русский

Принадлежность элементa к групоиду эквивалентна тому, что пара (e, source/target) удовлетворяет свойству pregrouppoid.

LaTeX

$$mem_groupoid_of_pregroupoid {PG : Pregroupoid H} {e : OpenPartialHomeomorph H H} : e ∈ PG.groupoid ↔ PG.property e e.source ∧ PG.property e.symm e.target$$

Lean4

theorem mem_groupoid_of_pregroupoid {PG : Pregroupoid H} {e : OpenPartialHomeomorph H H} :
    e ∈ PG.groupoid ↔ PG.property e e.source ∧ PG.property e.symm e.target :=
  Iff.rfl

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