Ioi_eq_biUnion — Mathlib

English

For densely ordered α and dense s, Ioi(x) is the union over y ∈ s ∩ Ioi(x) of Ioi(y).

Русский

Для плотно упорядоченного пространства Ioi(x) является объединением по y ∈ s ∩ Ioi(x) от Ioi(y).

LaTeX

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

Lean4

theorem Ioi_eq_biUnion [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) : Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y :=
  by
  refine Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))
  rcases hs.exists_between hz with ⟨y, hys, hxy, hyz⟩
  exact mem_iUnion₂.2 ⟨y, ⟨hys, hxy⟩, hyz⟩

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