classes_ker_subset_fiber_set — Mathlib

English

For any f: α → β, each equivalence class of the kernel of f is contained in some fiber { x ∈ α : f(x) = y } for some y ∈ β.

Русский

Для любого отображения f: α → β каждая эквив-класс Ker(f) содержится в некотором волокне { x ∈ α : f(x) = y } для некоторого y ∈ β.

LaTeX

$$$(\\ker f).\\mathrm{classes} \\subseteq \\{ \\{ x \\in α : f(x) = y \\} : y \\in β \\}.$$$

Lean4

theorem classes_ker_subset_fiber_set {β : Type*} (f : α → β) :
    (Setoid.ker f).classes ⊆ Set.range fun y => {x | f x = y} :=
  by
  rintro s ⟨x, rfl⟩
  rw [Set.mem_range]
  exact ⟨f x, rfl⟩

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