isInducing_prod_const — Mathlib

English

Let y ∈ Y and f: X → Z. Then IsInducing (λ x, (f x, y)) is equivalent to IsInducing f.

Русский

Пусть y ∈ Y и f: X → Z. Тогда IsInducing (λ x, (f x, y)) эквивалентно IsInducing f.

LaTeX

$$$\IsInducing(\lambda x: X, (f(x), y)) \iff \IsInducing(f)$$$

Lean4

@[simp]
theorem isInducing_prod_const {y : Y} {f : X → Z} : IsInducing (fun x => (f x, y)) ↔ IsInducing f := by
  simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose, Function.comp_def, induced_const,
    inf_top_eq]

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