gi_principal_ker — Mathlib

English

The principal operator and the kernel operator form a Galois coinsertion between Set α and Filter α: the relation 𝓟(s) ≤ f is equivalent to s ⊆ ker f.

Русский

Операторы π (множество → фильтр) и ядро образуют Galois-коинсерцию между множествами и фильтрами: 𝓟(s) ≤ f эквивалентно s ⊆ ker f.

LaTeX

$$$\\mathcal P(s) \\le f \\iff s \\subseteq \\ker f$$$

Lean4

/-- `Filter.principal` forms a Galois coinsertion with `Filter.ker`. -/
def gi_principal_ker : GaloisCoinsertion (𝓟 : Set α → Filter α) ker :=
  GaloisConnection.toGaloisCoinsertion (fun s f ↦ by simp [principal_le_iff]) <| by
    simp only [le_iff_subset, subset_def, mem_ker, mem_principal]; aesop

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