symm — Mathlib

English

If there exists an inverse relation InvOn f g, and f maps s bijectively onto t, then g maps t bijectively onto s.

Русский

Если существует обратная связь InvOn f g и f отображает s биективно в t, тогда g отображает t биективно в s.

LaTeX

$$$\\forall h:\\, InvOn f g t s \\to BijOn f s t \\to BijOn g t s$$$

Lean4

theorem symm {g : β → α} (h : InvOn f g t s) (hf : BijOn f s t) : BijOn g t s :=
  ⟨h.2.mapsTo hf.surjOn, h.1.injOn, h.2.surjOn hf.mapsTo⟩

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