biUnion_range_preimage_singleton — Mathlib

English

The union over all y in the range of f of the preimage of {y} equals the entire domain.

Русский

Объединение по y из образа f прообраза {y} даёт всю область определения.

LaTeX

$$$\bigcup_{y \in \operatorname{range}(f)} f^{-1}\{y\} = \mathrm{univ}$$$

Lean4

theorem biUnion_range_preimage_singleton (f : α → β) : ⋃ y ∈ range f, f ⁻¹' { y } = univ := by
  rw [biUnion_preimage_singleton, preimage_range]

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