isInducing_const_prod — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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