Ioc_inter_Ioo_of_right_le — Mathlib

English

If b2 ≤ b1, then Ioc(a1, b1) ∩ Ioo(a2, b2) = Ioo(max(a1, a2), b2).

Русский

Если b2 ≤ b1, то Ioc(a1, b1) ∩ Ioo(a2, b2) = Ioo(max(a1, a2), b2).

LaTeX

$$(b_2 \\le b_1) \\\\Rightarrow Ioc(a_1,b_1) \\cap Ioo(a_2,b_2) = Ioo(\\\\max(a_1,a_2), b_2)$$

Lean4

theorem Ioc_inter_Ioo_of_right_le (h : b₂ ≤ b₁) : Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) b₂ :=
  ext fun x => by simp [and_assoc, @and_left_comm (x ≤ _), and_iff_right_iff_imp.2 fun h' => (le_of_lt h').trans h]

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