cons_congr

Mathlib.Data.WSeq.Relation

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.cons_congr

English

If s ~ʷ t, then cons a s ~ʷ cons a t for any a.

Русский

Если s ~ʷ t, то для любого a верно cons a s ~ʷ cons a t.

LaTeX

$$$\forall \alpha\in,\ \forall a,\ s,t \in \mathrm{WSeq}(\alpha):\ s \sim_W t \Rightarrow \mathrm{cons}\ a\ s \sim_W \mathrm{cons}\ a\ t$$$

Lean4

theorem cons_congr {s t : WSeq α} (a : α) (h : s ~ʷ t) : cons a s ~ʷ cons a t := by unfold Equiv; simpa using h

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

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

Разделы

Аффилиация

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