bijOn_comm — Mathlib

English

BijOn maps are symmetric with respect to inverse relations: BijOn f s t is equivalent to BijOn g t s if g is the inverse on the sets.

Русский

BiOn отображения симметричны по отношению к обратной связи: BijOn f s t эквивалентно BijOn g t s, если g является обратной на этих множествах.

LaTeX

$$$BijOn f s t \\iff BijOn g t s$ (при условии InvOn f g t s)$$

Lean4

theorem bijOn_comm {g : β → α} (h : InvOn f g t s) : BijOn f s t ↔ BijOn g t s :=
  ⟨BijOn.symm h, BijOn.symm h.symm⟩

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