instDenselyOrderedForall — Mathlib

English

If each π(i) is densely ordered, then the dependent function space ∀ i, π(i) is densely ordered.

Русский

Если для каждого i множество π(i) плотно упорядочено, то пространство зависимых функций ∀ i, π(i) плотно упорядочено.

LaTeX

$$$DenselyOrdered(\forall i, \pi(i))$$$

Lean4

instance [∀ i, Preorder (π i)] [∀ i, DenselyOrdered (π i)] : DenselyOrdered (∀ i, π i) :=
  ⟨fun a b ↦ by
    classical
    simp_rw [Pi.lt_def]
    rintro ⟨hab, i, hi⟩
    obtain ⟨c, ha, hb⟩ := exists_between hi
    exact
      ⟨Function.update a i c, ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_self]⟩,
        update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_self]⟩⟩

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