map_σ

Mathlib.Data.Analysis.Filter

URI: https://scilib.ai/kg/mathlib#Filter.Realizer.map_σ

English

The index of the mapped realizer is unchanged: (F.map m).σ = F.σ.

Русский

Индекс реализатора после отображения остаётся тем же: (F.map m).σ = F.σ.

LaTeX

$$$(F.map m).\\sigma = F.\\sigma$.$$

Lean4

@[simp]
theorem map_σ (m : α → β) {f : Filter α} (F : f.Realizer) : (F.map m).σ = F.σ :=
  rfl

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

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

Разделы

Аффилиация

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