get?_congr

Mathlib.Data.WSeq.Relation

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.get?_congr

English

If s ~ʷ t, then for all n, get? s n ~ get? t n.

Русский

Если s ~ʷ t, то для любого n: get? s n ~ get? t n.

LaTeX

$$$\forall {s,t:\mathrm{WSeq}(\alpha)},\ s \sim_W t \rightarrow \forall n, (\mathrm{get?}\ s\ n) \sim (\mathrm{get?}\ t\ n)$$$

Lean4

theorem get?_congr {s t : WSeq α} (h : s ~ʷ t) (n) : get? s n ~ get? t n :=
  head_congr (dropn_congr h _)

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

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

Разделы

Аффилиация

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