comap_hasBasis

Mathlib.Order.Filter.Bases.Basic

URI: https://scilib.ai/kg/mathlib#Filter.comap_hasBasis

English

The comap of a filter has basis: (comap f l) has basis with sets s if s ∈ l.

Русский

Комап-фильтр имеет базис: (comap f l) имеет базис с множестами s, если s ∈ l.

LaTeX

$$$ HasBasis (comap f l) (\lambda s, s \in l) (\lambda s, f^{-1}(s)) $$$

Lean4

theorem comap_hasBasis (f : α → β) (l : Filter β) : HasBasis (comap f l) (fun s : Set β => s ∈ l) fun s => f ⁻¹' s :=
  ⟨fun _ => mem_comap⟩

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

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

Разделы

Аффилиация

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