exists_forall_pos_add_lt — Mathlib

English

In a canonically ordered additive setting on a finite index set, if x_i < y_i for all i, there exists a positive ε such that x_i + ε < y_i for all i.

Русский

В канонически упорядоченной аддитивной структуре над сколькими-либо индексов, если для всех i выполняется x_i < y_i, то существует положительное ε такое, что x_i + ε < y_i для всех i.

LaTeX

$$$\\exists\\epsilon>0\\;\\forall i:\\ x_i+\\epsilon

Lean4

theorem exists_forall_pos_add_lt [ExistsAddOfLE α] [Finite ι] {x y : ι → α} (h : ∀ i, x i < y i) :
    ∃ ε, 0 < ε ∧ ∀ i, x i + ε < y i := by
  cases nonempty_fintype ι
  cases isEmpty_or_nonempty ι
  · obtain ⟨a, ha⟩ := exists_ne (0 : α)
    obtain ha | ha := ha.lt_or_gt <;> obtain ⟨b, hb, -⟩ := exists_pos_add_of_lt' ha <;> exact ⟨b, hb, isEmptyElim⟩
  choose ε hε hxε using fun i => exists_pos_add_of_lt' (h i)
  obtain rfl : x + ε = y := funext hxε
  have hε : 0 < Finset.univ.inf' Finset.univ_nonempty ε := (Finset.lt_inf'_iff _).2 fun i _ => hε _
  obtain ⟨δ, hδ, hδε⟩ := exists_between hε
  exact ⟨δ, hδ, fun i ↦ add_lt_add_left (hδε.trans_le <| Finset.inf'_le _ <| Finset.mem_univ _) _⟩

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