inseparable_coe — Mathlib

English

Inseparability of maps is preserved by taking the coercion to functions: Inseparable (f) (g) for continuous maps f,g is equivalent to Inseparable (f) (g) when viewed as functions.

Русский

Неразделимость отображений сохраняется при переходе к их коэф-образам: неразделимость f и g как функций эквивалентна неразделимости их как непрерывных отображений.

LaTeX

$$$\\mathrm{Inseparable}(\\mathrm{coe}(f), \\mathrm{coe}(g)) \\iff \\mathrm{Inseparable}(f,g)$$$

Lean4

@[norm_cast]
theorem inseparable_coe {f g : C(X, Y)} : Inseparable (f : X → Y) g ↔ Inseparable f g := by
  simp only [inseparable_iff_specializes_and, specializes_coe]

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