ofWithBot_le — Mathlib

English

If every J ∈ boxes is below I, then the constructed prepartition is below or equal to π.

Русский

Если каждый J ∈ boxes ниже I, то сконструированное предразбиение ниже или равно π.

LaTeX

$$$ ofWithBot boxes \\; le\_of\\_mem \\; pairwise\\_disjoint ≤ π $$$

Lean4

theorem ofWithBot_le {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' ∈ π, J ≤ ↑J') : ofWithBot boxes le_of_mem pairwise_disjoint ≤ π :=
  by
  have : ∀ J : Box ι, ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J' := fun J hJ => by
    simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot
  simpa [ofWithBot, le_def]

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