English
If for every b ∈ β the preimage f^{-1}({b}) is either empty or all of α, and β is nonempty, then f is constant: there exists b ∈ β with f = const α b.
Русский
Если для каждого b ∈ β множество обратного образа f^{-1}({b}) либо пусто, либо все множество α, и β ненулевой, то функция f постоянна: существует b ∈ β такая, что f = константа b.
LaTeX
$$([Nonempty β] ∧ ∀ b ∈ β, f^{-1}({b}) = ∅ ∨ f^{-1}({b}) = α) ⇒ ∃ b ∈ β, ∀ x ∈ α, f(x) = b.$$
Lean4
/-- If preimage of each singleton under `f : α → β` is either empty or the whole type,
then `f` is a constant. -/
theorem exists_eq_const_of_preimage_singleton [Nonempty β] {f : α → β}
(hf : ∀ b : β, f ⁻¹' { b } = ∅ ∨ f ⁻¹' { b } = univ) : ∃ b, f = const α b :=
by
rcases em (∃ b, f ⁻¹' { b } = univ) with ⟨b, hb⟩ | hf'
· exact ⟨b, funext fun x ↦ eq_univ_iff_forall.1 hb x⟩
· have : ∀ x b, f x ≠ b := fun x b ↦ eq_empty_iff_forall_notMem.1 ((hf b).resolve_right fun h ↦ hf' ⟨b, h⟩) x
exact ⟨Classical.arbitrary β, funext fun x ↦ absurd rfl (this x _)⟩
