le_iff_nonempty_imp_le_and_iUnion_subset

English

A strong equivalence: π1 ≤ π2 iff a pairwise nonempty intersection implies box-wise order, and π1.iUnion ⊆ π2.iUnion.

Русский

Эквивалентность: π1 ≤ π2 эквивалентно тому, что для любых J ∈ π1 и J' ∈ π2, если J ∩ J' непусто, то J ≤ J', и дополнительно π1.iUnion ⊆ π2.iUnion.

LaTeX

$$π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, (J ∩ J' : Set(ι→ℝ)).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion$$

Lean4

theorem le_iff_nonempty_imp_le_and_iUnion_subset :
    π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, (J ∩ J' : Set (ι → ℝ)).Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion :=
  by
  constructor
  · refine fun H => ⟨fun J hJ J' hJ' Hne => ?_, iUnion_mono H⟩
    rcases H hJ with ⟨J'', hJ'', Hle⟩
    rcases Hne with ⟨x, hx, hx'⟩
    rwa [π₂.eq_of_mem_of_mem hJ' hJ'' hx' (Hle hx)]
  · rintro ⟨H, HU⟩ J hJ
    simp only [Set.subset_def, mem_iUnion] at HU
    rcases HU J.upper ⟨J, hJ, J.upper_mem⟩ with ⟨J₂, hJ₂, hx⟩
    exact ⟨J₂, hJ₂, H _ hJ _ hJ₂ ⟨_, J.upper_mem, hx⟩⟩

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