map_F

Mathlib.Data.Analysis.Filter

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

English

The value of the mapped realizer on s is the image of the original F.f s under m: (F.map m).F s = image m (F.F s).

Русский

Значение отображённого реализатора: (F.map m).F s = image m (F.F s).

LaTeX

$$$(F.map m).F\\,s = \\mathrm{image}\\ m (F.F\\,s)$.$$

Lean4

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

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

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

Разделы

Аффилиация

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