ofEquiv_val

Mathlib.Data.Analysis.Filter

URI: https://scilib.ai/kg/mathlib#CFilter.ofEquiv_val

English

For an equivalence E: σ ≃ τ, and a CFilter F: CFilter α σ, the transported base satisfies (F.ofEquiv E).f(a) = F.f(E.symm(a)).

Русский

Пусть E: σ ≃ τ. Тогда для CFilter F: CFilter α σ выполняется (F.ofEquiv E).f(a) = F.f(E.symm(a)).

LaTeX

$$$(F.ofEquiv E).f(a)=F.f(E^{-1}(a))$ for all $a\\in τ$.$$

Lean4

@[simp]
theorem ofEquiv_val (E : σ ≃ τ) (F : CFilter α σ) (a : τ) : F.ofEquiv E a = F (E.symm a) := by cases F; rfl

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

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

Разделы

Аффилиация

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