surjOn_iff_surjective — Mathlib

English

For a function f and subset s, SurjOn f s univ is equivalent to the restriction s.restrict f being surjective.

Русский

Для функции f и подмножества s, SurjOn f s univ эквивалентно сюръективности ограниченного отображения s.restrict f.

LaTeX

$$$\operatorname{SurjOn} f s \operatorname{univ} \;\iff\; \operatorname{Surjective}(s.restrict f)$$$

Lean4

theorem surjOn_iff_surjective : SurjOn f s univ ↔ Surjective (s.restrict f) :=
  ⟨fun H b =>
    let ⟨a, as, e⟩ := @H b trivial
    ⟨⟨a, as⟩, e⟩,
    fun H b _ =>
    let ⟨⟨a, as⟩, e⟩ := H b
    ⟨a, as, e⟩⟩

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