surjOn_iff — Mathlib

English

If EqOn f1 f2 on s, then SurjOn f1 s t is equivalent to SurjOn f2 s t.

Русский

Если f1 и f2 совпадают на s, то сюръективность на s→t для f1 эквивалентна сюръективности на s→t для f2.

LaTeX

$$$$ \\operatorname{EqOn}(f_1,f_2,s) \\Rightarrow \\big( \\operatorname{SurjOn}(f_1,s,t) \\iff \\operatorname{SurjOn}(f_2,s,t) \\big) $$$$

Lean4

theorem surjOn_iff (h : EqOn f₁ f₂ s) : SurjOn f₁ s t ↔ SurjOn f₂ s t :=
  ⟨fun H => H.congr h, fun H => H.congr h.symm⟩

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