disjiUnion_filter_eq_of_maps_to — Mathlib

English

If every element of s maps into t under f, then the disjiUnion of the fibers s.filter (f · = a) over a equals s.

Русский

Если каждый элемент множества s отображается в t функцией f, то дисjoint‑объединение волокон равняется s.

LaTeX

$$$\\forall x \\in s,\\ f x \\in t \\Rightarrow t.disjiUnion (\\lambda a \\mapsto s.filter (f \\cdot = a)) \\text{ pairwiseDisjoint_fibers } = s$$$

Lean4

theorem disjiUnion_filter_eq_of_maps_to (h : ∀ x ∈ s, f x ∈ t) :
    t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers = s := by simpa [filter_eq_self]

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