subset_kernImage_iff — Mathlib

English

For sets s,t and map f, s ⊆ kernImage f t iff f⁻¹' s ⊆ t.

Русский

Для множеств s,t и отображения f: s ⊆ kernImage f t эквивалентно f⁻¹' s ⊆ t.

LaTeX

$$$s \\subseteq \\operatorname{kernImage}(f,t) \\iff f^{-1}' s \\subseteq t$$$

Lean4

theorem subset_kernImage_iff {s : Set β} {t : Set α} {f : α → β} : s ⊆ kernImage f t ↔ f ⁻¹' s ⊆ t :=
  ⟨fun h _ hx ↦ h hx rfl, fun h _ hx y hy ↦ h (show f y ∈ s from hy.symm ▸ hx)⟩

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