biUnion_le_iff — Mathlib

English

Characterizes when the BiUnion is below a given prepartition π': it is equivalent to having πi J ≤ π'.restrict J for all J ∈ π.

Русский

Характеризует когда BiUnion ≤ π' : это эквивалентно тому, что для каждого J ∈ π выполняется πi J ≤ π'.restrict J.

LaTeX

$$$ π.biUnion π_i ≤ π' \\Longleftrightarrow \\forall J \\in π, π_i J ≤ π'.restrict J $$$

Lean4

theorem biUnion_le_iff {πi : ∀ J, Prepartition J} {π' : Prepartition I} :
    π.biUnion πi ≤ π' ↔ ∀ J ∈ π, πi J ≤ π'.restrict J :=
  by
  constructor <;> intro H J hJ
  · rw [← π.restrict_biUnion πi hJ]
    exact restrict_mono H
  · rw [mem_biUnion] at hJ
    rcases hJ with ⟨J₁, h₁, hJ⟩
    rcases H J₁ h₁ hJ with ⟨J₂, h₂, Hle⟩
    rcases π'.mem_restrict.mp h₂ with ⟨J₃, h₃, H⟩
    exact ⟨J₃, h₃, Hle.trans <| WithBot.coe_le_coe.1 <| H.trans_le inf_le_right⟩

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