English
For a1 < b1, the open interval Ioo(a1, b1) ⊆ Ioo(a2, b2) holds exactly when a2 ≤ a1 and b1 ≤ b2, under densely ordered assumptions.
Русский
Для a1 < b1 открытый интервал Ioo(a1, b1) содержится в Ioo(a2, b2) тогда и только тогда a2 ≤ a1 и b1 ≤ b2 при плотной упорядоченности.
LaTeX
$$$ a_1 < b_1 \Rightarrow ( (a_1, b_1) \subseteq (a_2, b_2) \iff a_2 \le a_1 \land b_1 \le b_2 )$$$
Lean4
theorem Ioo_subset_Ioo_iff [DenselyOrdered α] (h₁ : a₁ < b₁) : Ioo a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
⟨fun h => by
rcases exists_between h₁ with ⟨x, xa, xb⟩
constructor <;> refine le_of_not_gt fun h' => ?_
· have ab := (h ⟨xa, xb⟩).1.trans xb
exact lt_irrefl _ (h ⟨h', ab⟩).1
· have ab := xa.trans (h ⟨xa, xb⟩).2
exact lt_irrefl _ (h ⟨ab, h'⟩).2, fun ⟨h₁, h₂⟩ => Ioo_subset_Ioo h₁ h₂⟩
