eq_of_boxes_subset_iUnion_superset

English

If π1.boxes ⊆ π2.boxes and π2.iUnion ⊆ π1.iUnion, then π1 = π2.

Русский

Если π1.boxes ⊆ π2.boxes и π2.iUnion ⊆ π1.iUnion, то π1 = π2.

LaTeX

$$π₁.boxes ⊆ π₂.boxes ∧ π₂.iUnion ⊆ π₁.iUnion → π₁ = π₂$$

Lean4

theorem eq_of_boxes_subset_iUnion_superset (h₁ : π₁.boxes ⊆ π₂.boxes) (h₂ : π₂.iUnion ⊆ π₁.iUnion) : π₁ = π₂ :=
  le_antisymm (fun J hJ => ⟨J, h₁ hJ, le_rfl⟩) <|
    le_iff_nonempty_imp_le_and_iUnion_subset.2
      ⟨fun _ hJ₁ _ hJ₂ Hne => (π₂.eq_of_mem_of_mem hJ₁ (h₁ hJ₂) Hne.choose_spec.1 Hne.choose_spec.2).le, h₂⟩

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