Ico_filter_le_of_right_le — Mathlib

English

Let α be a preorder with LocallyFiniteOrder. Then there are no elements x in Ico(a,b) with x ≥ b; hence the intersection with {x | b ≤ x} is empty.

Русский

Пусть α обладает предеством с локально конечным порядком. В полуправильном интервале Ico(a,b) нет элементов x, удовлетворяющих x ≥ b; следовательно, {x ∈ Ico(a,b) | b ≤ x} = ∅.

LaTeX

$$$\{ x \in Ico(a,b) \mid b \le x \} = \emptyset$$$

Lean4

theorem Ico_filter_le_of_right_le {a b : α} [DecidablePred (b ≤ ·)] : {x ∈ Ico a b | b ≤ x} = ∅ :=
  filter_false_of_mem fun _ hx => (mem_Ico.1 hx).2.not_ge

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