mono — Mathlib

English

If s1 ⊆ s2, t1 ⊆ t2 and hf: SurjOn f s1 t2, then SurjOn f s2 t1.

Русский

Если s1 ⊆ s2, t1 ⊆ t2 и f образует сюръекцию с s1 на t2, то она образует сюръекцию с s2 на t1.

LaTeX

$$$$ (s_1 \\subseteq s_2) \\land (t_1 \\subseteq t_2) \\land \\operatorname{SurjOn}(f,s_1,t_2) \\Rightarrow \\operatorname{SurjOn}(f,s_2,t_1) $$$$

Lean4

theorem mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (hf : SurjOn f s₁ t₂) : SurjOn f s₂ t₁ :=
  Subset.trans ht <| Subset.trans hf <| image_mono hs

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