invOn_fixedPoints_comp — Mathlib

English

Any two maps f: α→β and g: β→α are inverse of each other on the corresponding fixed-point sets of f ∘ g and g ∘ f, respectively.

Русский

Любые две отображения f: α→β и g: β→α образуют взаимно обратные отображения на соответствующих множествах фиксированных точек f ∘ g и g ∘ f.

LaTeX

$$$Set.InvOn f g (fixedPoints (f\circ g)) (fixedPoints (g\circ f))$$$

Lean4

/-- Any two maps `f : α → β` and `g : β → α` are inverse of each other on the sets of fixed points
of `f ∘ g` and `g ∘ f`, respectively. -/
theorem invOn_fixedPoints_comp (f : α → β) (g : β → α) : Set.InvOn f g (fixedPoints <| f ∘ g) (fixedPoints <| g ∘ f) :=
  ⟨fun _ => id, fun _ => id⟩

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