inseparable_coe — Mathlib

English

Inseparability is preserved under the OnePoint embedding: Inseparable (x:OnePoint X) y iff Inseparable x y.

Русский

Неразделимость сохраняется под вложением OnePoint: Inseparable( x:OnePoint X, y ) ↔ Inseparable(x,y).

LaTeX

$$$\\operatorname{Inseparable}((x: \\mathrm{OnePoint} X), y) \\iff \\operatorname{Inseparable}(x,y).$$$

Lean4

@[simp, norm_cast]
theorem inseparable_coe {x y : X} : Inseparable (x : OnePoint X) y ↔ Inseparable x y :=
  isOpenEmbedding_coe.isInducing.inseparable_iff

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