of_comp_iff — Mathlib

English

If g is inducing, then IsInducing(g ∘ f) holds iff IsInducing f holds.

Русский

Если g индуцирующее, то IsInducing(g ∘ f) эквивалентно IsInducing f.

LaTeX

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

Lean4

theorem of_comp_iff (hg : IsInducing g) : IsInducing (g ∘ f) ↔ IsInducing f :=
  by
  refine ⟨fun h ↦ ?_, hg.comp⟩
  rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]

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