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⟩