eventually_isPartition — Mathlib

English

For l and box I, eventually every π in l.toFilteriUnion I ⊤ is a partition.

Русский

Для l и Box I в пределе почти каждый элемент π в l.toFilteriUnion I ⊤ является разбиением.

LaTeX

$$∀ᶠ π in l.toFilteriUnion I ⊤, TaggedPrepartition.IsPartition π$$

Lean4

theorem eventually_isPartition (l : IntegrationParams) (I : Box ι) :
    ∀ᶠ π in l.toFilteriUnion I ⊤, TaggedPrepartition.IsPartition π :=
  eventually_iSup.2 fun _ =>
    eventually_inf_principal.2 <|
      Eventually.of_forall fun π h => π.isPartition_iff_iUnion_eq.2 (h.trans Prepartition.iUnion_top)

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