Ioo_filter_lt — Mathlib

English

Let α be a linearly ordered set in which all intervals Ioo(a,b) are finite. Then for any a,b,c ∈ α, the subset of x in Ioo(a,b) with x < c is exactly Ioo(a, min(b,c)).

Русский

Пусть α — линейно упорядоченное множество, в котором каждый интервал Ioo(a,b) конечен. Тогда для любые a,b,c ∈ α множество x ∈ Ioo(a,b) и удовлетворяющее x < c равно Ioo(a, min(b,c)).

LaTeX

$$$\{x \in Ioo(a,b) \mid x < c\} = Ioo(a, \min\{b,c\})$$$

Lean4

@[simp]
theorem Ioo_filter_lt (a b c : α) : {x ∈ Ioo a b | x < c} = Ioo a (min b c) :=
  by
  ext
  simp [and_assoc]

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