kernMap_principal — Mathlib

English

For any subset s of α, kernMap m (principal s) equals principal (kernImage m s).

Русский

Для любого подмножества s ⊆ α выполняется kernMap m (principal s) = principal (kernImage m s).

LaTeX

$$$\\operatorname{kernMap}(m, \\mathcal{P}(s)) = \\mathcal{P}(\\operatorname{kernImage}(m, s))$$$

Lean4

theorem kernMap_principal {s : Set α} : kernMap m (𝓟 s) = 𝓟 (kernImage m s) :=
  by
  refine eq_of_forall_le_iff (fun g ↦ ?_)
  rw [← comap_le_iff_le_kernMap, le_principal_iff, le_principal_iff, mem_comap'']

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