of_comp_iff — Mathlib

English

If g is IsUniformInducing and f is any map, then IsUniformInducing (g ∘ f) iff IsUniformInducing f (composition preserves inducing property).

Русский

Если g — IsUniformInducing, то IsUniformInducing (g ∘ f) эквивалентно IsUniformInducing f.

LaTeX

$$$IsUniformInducing (g \\circ f) \\iff IsUniformInducing f$$$

Lean4

theorem of_comp_iff {g : β → γ} (hg : IsUniformInducing g) {f : α → β} :
    IsUniformInducing (g ∘ f) ↔ IsUniformInducing f :=
  by
  refine ⟨fun h ↦ ?_, hg.comp⟩
  rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity, Function.comp_def,
    Function.comp_def]

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