Iio_filter_lt — Mathlib

English

In a linear order with a bottom element, for any a,b ∈ α, the set {x ∈ Iio(a) | x < b} equals Iio(min(a,b)).

Русский

В линейном порядке с нижней границей для любых a,b ∈ α множество x ∈ Iio(a) и x < b равно Iio(min(a,b)).

LaTeX

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

Lean4

@[simp]
theorem Iio_filter_lt {α} [LinearOrder α] [LocallyFiniteOrderBot α] (a b : α) : {x ∈ Iio a | x < b} = Iio (min a b) :=
  by
  ext
  simp

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