surjOn — Mathlib

English

If a morphism f has SurjectiveOnWith on K with C, then it is surjective on K from univ to K as a function between sets.

Русский

Если у отображения f есть свойство SurjectiveOnWith на K с C, то оно действует как сюръективное на K между соответствующими множествами.

LaTeX

$$$ f.SurjectiveOnWith\\ K\\ C \\Rightarrow Set.SurjOn (\\text{NormedAddGroupHom.funLike.coe } f) Set.univ (AddSubgroup.instSetLike.coe K)$$$

Lean4

theorem surjOn {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C : ℝ} (h : f.SurjectiveOnWith K C) :
    Set.SurjOn f Set.univ K := fun x hx => (h x hx).imp fun _a ⟨ha, _⟩ => ⟨Set.mem_univ _, ha⟩

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