Icc_filter_lt_of_lt_right — Mathlib

English

If b < c, then every x ∈ Icc(a,b) satisfies x < c; thus filtering by x < c yields Icc(a,b).

Русский

Если b < c, то для всех x ∈ Icc(a,b) выполняется x < c; поэтому фильтрация по x < c даёт Icc(a,b).

LaTeX

$$$ b < c \Rightarrow \{ x \in Icc(a,b) \mid x < c \} = Icc(a,b) $$$

Lean4

theorem Icc_filter_lt_of_lt_right {a b c : α} [DecidablePred (· < c)] (h : b < c) : {x ∈ Icc a b | x < c} = Icc a b :=
  filter_true_of_mem fun _ hx => lt_of_le_of_lt (mem_Icc.1 hx).2 h

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