congr — Mathlib

English

If h: SurjOn f1 s t and H: EqOn f1 f2 s, then SurjOn f2 s t.

Русский

Если f1 и f2 совпадают на s и f1 образует сюръекцию на t от s, то и f2 образует сюръекцию на t от s.

LaTeX

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

Lean4

theorem congr (h : SurjOn f₁ s t) (H : EqOn f₁ f₂ s) : SurjOn f₂ s t := by rwa [SurjOn, ← H.image_eq]

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