Ico_subset_Ico_iff — Mathlib

English

If a1 < b1, then Ico(a1,b1) ⊆ Ico(a2,b2) if and only if a2 ≤ a1 and b1 ≤ b2.

Русский

Пусть a1 < b1. Тогда Ico(a1,b1) ⊆ Ico(a2,b2) тогда и только тогда, когда a2 ≤ a1 и b1 ≤ b2.

LaTeX

$$$ Ico(a_1,b_1) \subseteq Ico(a_2,b_2) \iff a_2 \le a_1 \wedge 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₂ :=
  Finset.Ico_subset_Ico_iff h

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