surjOn — Mathlib

English

If h is a left inverse on s, then f''(s₁ ∩ s) equals f'^{-1}(s₁ ∩ s) ∩ f''s.

Русский

Если h — левый обратный на s, то образ(f) от пересечения s₁ ∩ s равен пересечению f'^{-1}(s₁ ∩ s) и образу s.

LaTeX

$$$$ f '' (s_1 \\cap s) = f'^{-1}' (s_1 \\cap s) \\cap f '' s. $$$$

Lean4

theorem surjOn (h : LeftInvOn f' f s) (hf : MapsTo f s t) : SurjOn f' t s := fun x hx => ⟨f x, hf hx, h hx⟩

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