ker_comap — Mathlib

English

For any map m: α → β and filter f on β, ker (comap m f) equals the preimage of ker f under m: ker (comap m f) = m^{-1}(ker f).

Русский

Для отображения m: α → β и фильтра f на β, ker(comap m f) равно предобразу ker f по m: ker(comap m f) = m^{-1}(ker f).

LaTeX

$$$\\ker(\\mathrm{comap}\\, m\\, f) = m^{-1}\\,'\\ker f$$$

Lean4

@[simp]
theorem ker_comap (m : α → β) (f : Filter β) : ker (comap m f) = m ⁻¹' ker f :=
  by
  ext a
  simp only [mem_ker, mem_comap, forall_exists_index, and_imp, @forall_swap (Set α), mem_preimage]
  exact forall₂_congr fun s _ ↦ ⟨fun h ↦ h _ Subset.rfl, fun ha t ht ↦ ht ha⟩

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