equivalence — Mathlib

English

If r is an equivalence relation on β and f: α → β, then the pullback InvImage r f defines an equivalence relation on α.

Русский

Если r — эквивалентность на β и f: α → β, то тягловая по отношению r через f образует эквивалентность на α.

LaTeX

$$Equivalence (InvImage r f)$$

Lean4

theorem equivalence {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) (h : Equivalence r) :
    Equivalence (InvImage r f) :=
  ⟨fun _ ↦ h.1 _, h.symm, h.trans⟩

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