mem_kernMap_iff_compl — Mathlib

English

For s ⊆ β, s ∈ kernMap m f iff ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ.

Русский

Для множества s ⊆ β верно: s принадлежит kernMap m f тогда, когда существует t такое, что tᶜ ∈ f и m '' t = sᶜ.

LaTeX

$$$s \\in \\operatorname{kernMap}(m,f) \\iff \\exists t, t^{\\complement} \\in f \\land m '' t = s^{\\complement}$$$

Lean4

theorem mem_kernMap_iff_compl {s : Set β} : s ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ :=
  by
  rw [mem_kernMap, compl_surjective.exists]
  refine exists_congr (fun x ↦ and_congr_right fun _ ↦ ?_)
  rw [kernImage_compl, compl_eq_comm, eq_comm]

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