snd

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#Specializes.snd

English

If (a,b) specializes to (a',b'), then b specializes to b'.

Русский

Если пара (a,b) специализируется на (a',b'), то вторая координата специализируется на b'.

LaTeX

$$$$ (a,b) \rightsquigarrow (a',b') \Rightarrow b \rightsquigarrow b'. $$$$

Lean4

theorem snd {a b : X × Y} (h : a ⤳ b) : a.2 ⤳ b.2 :=
  (specializes_prod.1 h).2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru