coe_restrict_apply

Mathlib.Dynamics.Flow

URI: https://scilib.ai/kg/mathlib#Flow.coe_restrict_apply

English

For invariant set s, (restrict φ s) t x = φ t x.

Русский

Для инвариантного множества s выполняется (restrict φ s) t x = φ t x.

LaTeX

$$$((\restrict \varphi s) t x) = \varphi t x$$$

Lean4

@[simp]
theorem coe_restrict_apply {s : Set α} (h : IsInvariant ϕ s) (t : τ) (x : s) : restrict ϕ h t x = ϕ t x :=
  rfl

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

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

Разделы

Аффилиация

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