le_iff — Mathlib

English

If π2 is a partition, then π1 ≤ π2 if and only if for every J in π1 and J' in π2, whenever J ∩ J' is nonempty, one has J ⊆ J'.

Русский

Если π2 — разбиение, то π1 ≤ π2 тогда и только тогда, когда для любых J ∈ π1 и J' ∈ π2, если J ∩ J' ≠ ∅, то J ⊆ J'.

LaTeX

$$$\\pi_2 \\text{IsPartition} \\Rightarrow (\\pi_1 \\le \\pi_2) \\iff \\forall J \\in \\pi_1, \\forall J' \\in \\pi_2, (J \\cap J' \\neq \\emptyset) \\Rightarrow (J \\subseteq J').$$$

Lean4

theorem le_iff (h : π₂.IsPartition) : π₁ ≤ π₂ ↔ ∀ J ∈ π₁, ∀ J' ∈ π₂, (J ∩ J' : Set (ι → ℝ)).Nonempty → J ≤ J' :=
  le_iff_nonempty_imp_le_and_iUnion_subset.trans <| and_iff_left <| h.iUnion_subset _

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