mem_kernMap — Mathlib

English

For s ⊆ β, s belongs to kernMap m f iff there exists t ∈ f with kernImage m t = s.

Русский

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

LaTeX

$$$s \\in \\operatorname{kernMap}(m,f) \\iff \\exists t \\in f,\\ \\operatorname{kernImage}(m,t) = s$$$

Lean4

theorem mem_kernMap {s : Set β} : s ∈ kernMap m f ↔ ∃ t ∈ f, kernImage m t = s :=
  Iff.rfl

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