Ico_filter_le_of_le_left — Mathlib

English

If a2 ≤ b2, a2 ≤ a1, and b1 < b2, then Icc(a1, b1) is strictly contained in Icc(a2, b2).

Русский

Если a2 ≤ b2, a2 ≤ a1 и b1 < b2, то Icc(a1,b1) ⊂ Icc(a2,b2).

LaTeX

$$$ (a_2 \le b_2) \land (a_2 \le a_1) \land (b_1 < b_2) \Rightarrow Icc(a_1,b_1) \subset Icc(a_2,b_2) $$$

Lean4

theorem Ico_filter_le_of_le_left {a b c : α} [DecidablePred (c ≤ ·)] (hca : c ≤ a) : {x ∈ Ico a b | c ≤ x} = Ico a b :=
  filter_true_of_mem fun _ hx => hca.trans (mem_Ico.1 hx).1

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