comp — Mathlib

English

Let s ⊆ α, t ⊆ β, p ⊆ γ and f: α → β, g: β → γ. If f maps s onto t and g maps t onto p, then the composition g ∘ f maps s onto p.

Русский

Пусть s ⊆ α, t ⊆ β, p ⊆ γ и f: α → β, g: β → γ. Если f отображает s на t и g отображает t на p, тогда композиция g ∘ f отображает s на p.

LaTeX

$$$ (\mathrm{SurjOn}(g) t p) \wedge (\mathrm{SurjOn}(f) s t) \rightarrow \mathrm{SurjOn}(g\circ f) s p $$$

Lean4

theorem comp (hg : SurjOn g t p) (hf : SurjOn f s t) : SurjOn (g ∘ f) s p :=
  Subset.trans hg <| Subset.trans (image_mono hf) <| image_comp g f s ▸ Subset.refl _

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