specializes_coe — Mathlib

English

Specialization is preserved under the canonical embedding: (x: X) ⤳ y iff (x: OnePoint X) ⤳ y.

Русский

Специализация сохраняется под каноническим вложением: (x) ⤳ y в X эквивалентно (x) ⤳ y в OnePoint X.

LaTeX

$$$ (x: X) \\!\\uparrow\\\\! y \\iff (x: \\mathrm{OnePoint}X) \\!\\uparrow\\\\! y. $$$

Lean4

@[simp, norm_cast]
theorem specializes_coe {x y : X} : (x : OnePoint X) ⤳ y ↔ x ⤳ y :=
  isOpenEmbedding_coe.isInducing.specializes_iff

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