English
Let ι be finite and f: ι → α. There exists a g: ι → α with g ≤ f, univ.sup g = univ.sup f, and g is pairwise disjoint.
Русский
Пусть ι конечно, и f:ι→α. Существование g:ι→α такое, что g ≤ f, sup g по всей единице равен sup f по всей единице, и g попарно взаимно непересекаются.
LaTeX
$$$\exists g:\ ι \to α,\; (\forall i,\ g(i) \le f(i)) \\ \land\; \operatorname{univ}.\operatorname{sup} g = \operatorname{univ}.\operatorname{sup} f \\ \land\; \operatorname{Pairwise}(\operatorname{Disjoint} on\ g)$$$
Lean4
/-- For any finite family of elements `f : ι → α`, we can find a pairwise-disjoint family `g`
bounded above by `f` and having the same supremum. This is non-canonical, depending on an arbitrary
choice of ordering of `ι`. -/
theorem exists_disjointed_le {ι : Type*} [Fintype ι] (f : ι → α) :
∃ g, g ≤ f ∧ univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g) :=
by
rcases isEmpty_or_nonempty ι with hι | hι
· -- do `ι = ∅` separately since `⊤ : Fin n` isn't defined for `n = 0`
exact ⟨f, le_rfl, rfl, Subsingleton.pairwise⟩
let R : ι ≃ Fin _ := equivFin ι
let f' : Fin _ → α := f ∘ R.symm
have hf' : f = f' ∘ R := by ext; simp only [Function.comp_apply, Equiv.symm_apply_apply, f']
refine ⟨disjointed f' ∘ R, ?_, ?_, ?_⟩
· intro n
simpa only [hf'] using disjointed_le f' (R n)
· simpa only [← sup_image, image_univ_equiv, hf'] using sup_disjointed f'
· exact fun i j hij ↦ disjoint_disjointed f' (R.injective.ne hij)
