restrict_surjective_iff — Mathlib

English

Another standard formulation: SurjOn f s univ is equivalent to the surjectivity of s.restrict f.

Русский

Еще одно стандартное формулирование: SurjOn f s univ эквивалентно сюръективности s.restrict f.

LaTeX

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

Lean4

@[simp]
theorem restrict_surjective_iff (h : MapsTo f s t) : Surjective (MapsTo.restrict _ _ _ h) ↔ SurjOn f s t :=
  by
  refine ⟨fun h' b hb ↦ ?_, fun h' ⟨b, hb⟩ ↦ ?_⟩
  · obtain ⟨⟨a, ha⟩, ha'⟩ := h' ⟨b, hb⟩
    replace ha' : f a = b := by simpa [Subtype.ext_iff] using ha'
    rw [← ha']
    exact mem_image_of_mem f ha
  · obtain ⟨a, ha, rfl⟩ := h' hb
    exact ⟨⟨a, ha⟩, rfl⟩

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