Ico_filter_le_left — Mathlib

English

Let a < b in a locally finite ordered set. The elements of the half-open interval [a,b) that also satisfy x ≤ a consist only of a; i.e., (Ico(a,b) ∩ (-∞, a]) = {a}.

Русский

Пусть a < b в локально конечном порядке. Элементы полуоткрытого интервала [a,b), удовлетворяющие x ≤ a, образуют единственный элемент a: (Ico(a,b) ∩ (-∞, a]) = {a}.

LaTeX

$$$ a < b \Rightarrow Ico(a,b) \cap (-\infty, a] = \{a\} $$$

Lean4

theorem Ico_filter_le_left {a b : α} [DecidablePred (· ≤ a)] (hab : a < b) :
    ((Ico a b).filter fun x => x ≤ a) = { a } :=
  by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]
  rfl

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