ultrafilter_extend_pure

Mathlib.Topology.Compactification.StoneCech

URI: https://scilib.ai/kg/mathlib#ultrafilter_extend_pure

English

For any a ∈ α, Ultrafilter.extend f (pure a) = f a.

Русский

Для любого a ∈ α выполняется Ultrafilter.extend f (pure a) = f a.

LaTeX

$$$Ultrafilter\.extend\ f\ (Ultrafilter\.instPure\.pure\ a) = f\ a$$$

Lean4

@[simp]
theorem ultrafilter_extend_pure (f : α → γ) (a : α) : Ultrafilter.extend f (pure a) = f a :=
  congr_fun (ultrafilter_extend_extends f) a

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

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

Разделы

Аффилиация

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