bijective_iff_bijOn_univ — Mathlib

English

If g is bijective on t to p and f is bijective on s to t, then g ∘ f is bijective on s to p.

Русский

Если g.biективна на t→p, а f биективна на s→t, тогда g∘f биективна на s→p.

LaTeX

$$$\\text{BijOn}(g,t,p)\\land\\text{BijOn}(f,s,t) \\Rightarrow \\text{BijOn}(g\\circ f,s,p)$$$

Lean4

theorem bijective_iff_bijOn_univ : Bijective f ↔ BijOn f univ univ :=
  Iff.intro
    (fun h =>
      let ⟨inj, surj⟩ := h
      ⟨mapsTo_univ f _, inj.injOn, Iff.mp surjective_iff_surjOn_univ surj⟩)
    fun h =>
    let ⟨_map, inj, surj⟩ := h
    ⟨Iff.mpr injective_iff_injOn_univ inj, Iff.mpr surjective_iff_surjOn_univ surj⟩

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