of_comp — Mathlib

English

If f and g are continuous and g ∘ f is inducing, then f is inducing.

Русский

Если f и g непрерывны, а g ∘ f индуцирующее, то f индуцирующее.

LaTeX

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

Lean4

theorem of_comp (hf : Continuous f) (hg : Continuous g) (hgf : IsInducing (g ∘ f)) : IsInducing f :=
  ⟨le_antisymm hf.le_induced (by grw [hgf.eq_induced, ← induced_compose, ← hg.le_induced])⟩

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