English
If every J ∈ boxes1 can be extended to some J' ∈ boxes2 with J ≤ J', then the corresponding ofWithBot objects are ordered: ofWithBot boxes1 ≤ ofWithBot boxes2.
Русский
Если каждый J ∈ boxes1 может быть продолжен до некоторого J' ∈ boxes2 с J ≤ J', то соответствующие конструкции ofWithBot удовлетворяют неравенству: boxes1 ≤ boxes2.
LaTeX
$$$ (∀ J ∈ boxes_1, J \\neq ⊥ → ∃ J' ∈ boxes_2, J ≤ J') \\\\Rightarrow ofWithBot boxes_1 le\_ofWithBot boxes_2 $$$
Lean4
theorem ofWithBot_mono {boxes₁ : Finset (WithBot (Box ι))} {le_of_mem₁ : ∀ J ∈ boxes₁, (J : WithBot (Box ι)) ≤ I}
{pairwise_disjoint₁ : Set.Pairwise (boxes₁ : Set (WithBot (Box ι))) Disjoint} {boxes₂ : Finset (WithBot (Box ι))}
{le_of_mem₂ : ∀ J ∈ boxes₂, (J : WithBot (Box ι)) ≤ I}
{pairwise_disjoint₂ : Set.Pairwise (boxes₂ : Set (WithBot (Box ι))) Disjoint}
(H : ∀ J ∈ boxes₁, J ≠ ⊥ → ∃ J' ∈ boxes₂, J ≤ J') :
ofWithBot boxes₁ le_of_mem₁ pairwise_disjoint₁ ≤ ofWithBot boxes₂ le_of_mem₂ pairwise_disjoint₂ :=
le_ofWithBot _ fun J hJ => H J (mem_ofWithBot.1 hJ) WithBot.coe_ne_bot
