Documentation

Mathlib.Algebra.Order.Field.Pi

Lemmas about (finite domain) functions into fields. #

We split this from Algebra.Order.Field.Basic to avoid importing the finiteness hierarchy there.

theorem Pi.exists_forall_pos_add_lt {α : Type u_1} {ι : Type u_2} [LinearOrderedCancelAddCommMonoid α] [Nontrivial α] [DenselyOrdered α] [ExistsAddOfLE α] [Finite ι] {x : ια} {y : ια} (h : ∀ (i : ι), x i < y i) :
∃ (ε : α), 0 < ε ∀ (i : ι), x i + ε < y i