Ico_subset_Ico_iff — Mathlib

English

For all a1 < b1 in a linear order with local finiteness, Ico(a1,b1) ⊆ Ico(a2,b2) iff a2 ≤ a1 and b1 ≤ b2.

Русский

Пусть задан линейный порядок и локальная конечность. Тогда Ico(a1,b1) ⊆ Ico(a2,b2) тогда и только тогда, когда a2 ≤ a1 и b1 ≤ b2 (при условии a1 < b1).

LaTeX

$$$ Ico(a_1,b_1) \subseteq Ico(a_2,b_2) \iff a_2 \le a_1 \land b_1 \le b_2 \quad (a_1 < b_1) $$$

Lean4

theorem Ico_subset_Ico_iff {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) : Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ := by
  rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]

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