Ioc_inter_Ioo_of_left_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem Ioc_inter_Ioo_of_left_lt (h : b₁ < b₂) : Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁ :=
  ext fun x => by simp [and_assoc, @and_left_comm (x ≤ _), and_iff_left_iff_imp.2 fun h' => lt_of_le_of_lt h' h]

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