English
If for every J ∈ π there exists J' ∈ boxes with J ≤ J', then π ≤ ofWithBot boxes le_of_mem pairwise_disjoint.
Русский
Если для каждого J ∈ π существует J' ∈ boxes с J ≤ J', то π ≤ ofWithBot boxes le_of_mem pairwise_disjoint.
LaTeX
$$$ (\\forall J \\in π, \\exists J' \\in boxes, J \\le J') \\Rightarrow π \\le ofWithBot boxes le\_of\\_mem pairwise\\_disjoint $$$
Lean4
theorem le_ofWithBot {boxes : Finset (WithBot (Box ι))} {le_of_mem : ∀ J ∈ boxes, (J : WithBot (Box ι)) ≤ I}
{pairwise_disjoint : Set.Pairwise (boxes : Set (WithBot (Box ι))) Disjoint} (H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J') :
π ≤ ofWithBot boxes le_of_mem pairwise_disjoint :=
by
intro J hJ
rcases H J hJ with ⟨J', J'mem, hle⟩
lift J' to Box ι using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hle
exact ⟨J', mem_ofWithBot.2 J'mem, WithBot.coe_le_coe.1 hle⟩
