Iio_eq_biUnion — Mathlib

English

Dual to Ioi_eq_biUnion: Iio(x) equals the union over y ∈ s ∩ Iio(x) of Iio(y).

Русский

Дуал к Ioi_eq_biUnion: Iio(x) равно объединению по y ∈ s ∩ Iio(x) от Iio(y).

LaTeX

$$$[DenselyOrdered\ α]\;\text{Dense } s\;\Rightarrow\; Iio(x)=\bigcup_{y\in s\cap Iio(x)} Iio(y).$$$

Lean4

theorem Iio_eq_biUnion [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) : Iio x = ⋃ y ∈ s ∩ Iio x, Iio y :=
  Dense.Ioi_eq_biUnion (α := αᵒᵈ) hs x

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