English
Let h be a FineSubfamilyOn f s. There exists a set t of pairs (x, A) with A ∈ v.setsAt(x) ∩ f(x) such that every pair's x-coordinate lies in s, the second components A are pairwise disjoint, each A belongs to v.setsAt(x) ∩ f(x), and μ of the uncovered part s \\ ⋃_{p∈t} p.2 is zero.
Русский
Пусть h — тонкое подпсемейство f на s. Существует множество t пар (x, A) such that A ∈ v.setsAt(x) ∩ f(x), все x-координаты лежат в s, множества A попарно не пересекаются, и каждый A принадлежит соответствующей паре, а мера оставшейся части s, не покрытой ⋃_{p∈t} p.2, равна нулю.
LaTeX
$$$\\exists t\\subseteq X\\times\\mathrm{Set}X\\;\\Big(\\forall p\\in t\\, p.1\\in s\\Big)\\land \\Big(t.PAIRWISEDISJOINT(p.2)\\Big)\\land \\Big(\\forall p\\in t\\, p.2\\in v.setsAt(p.1)\\cap f(p.1)\\Big)\\land \\mu\\Bigl(s\\setminus\\bigcup_{p\\in t} p.2\\Bigr)=0.$$$
Lean4
theorem exists_disjoint_covering_ae :
∃ t : Set (X × Set X),
(∀ p : X × Set X, p ∈ t → p.1 ∈ s) ∧
(t.PairwiseDisjoint fun p => p.2) ∧
(∀ p : X × Set X, p ∈ t → p.2 ∈ v.setsAt p.1 ∩ f p.1) ∧ μ (s \ ⋃ (p : X × Set X) (_ : p ∈ t), p.2) = 0 :=
v.covering s (fun x => v.setsAt x ∩ f x) (fun _ _ => inter_subset_left) h
