bijOn' — Mathlib

English

If e maps s into t and e.symm maps t into s, then e is a bijection between s and t.

Русский

Если отображение e отправляет s в t, а обратное e.symm отображает t обратно в s, тогда e является биекция между s и t.

LaTeX

$$$ \\operatorname{MapsTo} e s t \\Rightarrow \\operatorname{MapsTo} e^{-1} t s \\Rightarrow \\operatorname{BijOn} e s t. $$$

Lean4

theorem bijOn' (h₁ : MapsTo e s t) (h₂ : MapsTo e.symm t s) : BijOn e s t :=
  ⟨h₁, e.injective.injOn, fun b hb ↦ ⟨e.symm b, h₂ hb, apply_symm_apply _ _⟩⟩

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