compl_mem_kernMap — 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^{\\complement} \\in \\operatorname{kernMap}(m,f) \\iff \\exists t, t^{\\complement} \\in f ∧ m '' t = s$$$

Lean4

theorem compl_mem_kernMap {s : Set β} : sᶜ ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s := by
  simp_rw [mem_kernMap_iff_compl, compl_compl]

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