disjoint_boxes_of_disjoint_iUnion

English

If Disjoint π1.iUnion π2.iUnion, then Disjoint π1.boxes π2.boxes.

Русский

Если π1.iUnion и π2.iUnion непротиворазделимы, то π1.boxes и π2.boxes также непересекаются.

LaTeX

$$Disjoint π₁.iUnion π₂.iUnion → Disjoint π₁.boxes π₂.boxes$$

Lean4

theorem disjoint_boxes_of_disjoint_iUnion (h : Disjoint π₁.iUnion π₂.iUnion) : Disjoint π₁.boxes π₂.boxes :=
  Finset.disjoint_left.2 fun J h₁ h₂ =>
    Disjoint.le_bot (h.mono (π₁.subset_iUnion h₁) (π₂.subset_iUnion h₂)) ⟨J.upper_mem, J.upper_mem⟩

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