Lemmas about (finite domain) functions into fields. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [linear_ordered_semifield α] [has_exists_add_of_le α] [finite ι] {x y : ι → α} (h : ∀ (i : ι), x i < y i) :

∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i