comp — Mathlib

English

If g and f are inducing maps, then their composition g ∘ f is inducing.

Русский

Если отображения g и f индуцирующие, то их композиция g ∘ f индуцирующая.

LaTeX

$$$\operatorname{IsInducing}(g) \land \operatorname{IsInducing}(f) \Rightarrow \operatorname{IsInducing}(g \circ f).$$$

Lean4

protected theorem comp (hg : IsInducing g) (hf : IsInducing f) : IsInducing (g ∘ f) :=
  ⟨by rw [hf.eq_induced, hg.eq_induced, induced_compose]⟩

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