think_congr

Mathlib.Data.WSeq.Relation

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

English

If s ~ʷ t, then think s ~ʷ think t.

Русский

Если s ~ʷ t, то think s ~ʷ think t.

LaTeX

$$$\forall s,t\in \mathrm{WSeq}(\alpha),\ s \sim_W t \rightarrow \mathrm{think}(s) \sim_W \mathrm{think}(t)$$$

Lean4

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

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

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

Разделы

Аффилиация

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