From ef0ef216448e5943595a62a20b5461e00738f39b Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sat, 5 Nov 2022 04:51:25 +0000 Subject: [PATCH] chore(algebra/order/field): don't import finiteness hierarchy (#17350) This problem was just introduced in #16971. Hopefully we can all be careful about not adding heavy imports to fundamental files. Co-authored-by: Scott Morrison --- .../computation/basic.lean | 2 +- src/algebra/order/absolute_value.lean | 2 +- .../order/{field.lean => field/basic.lean} | 18 ++---------- .../{field_defs.lean => field/defs.lean} | 2 +- src/algebra/order/field/pi.lean | 28 +++++++++++++++++++ src/algebra/order/positive/field.lean | 2 +- src/algebra/order/smul.lean | 2 +- src/analysis/special_functions/bernstein.lean | 2 +- src/analysis/specific_limits/normed.lean | 2 +- src/data/nat/cast_field.lean | 2 +- src/data/nat/choose/bounds.lean | 2 +- src/data/rat/order.lean | 2 +- src/data/set/intervals/image_preimage.lean | 2 +- src/order/filter/at_top_bot.lean | 2 +- 14 files changed, 42 insertions(+), 28 deletions(-) rename src/algebra/order/{field.lean => field/basic.lean} (98%) rename src/algebra/order/{field_defs.lean => field/defs.lean} (98%) create mode 100644 src/algebra/order/field/pi.lean diff --git a/src/algebra/continued_fractions/computation/basic.lean b/src/algebra/continued_fractions/computation/basic.lean index 5780fcc8ca078..631babbee4a98 100644 --- a/src/algebra/continued_fractions/computation/basic.lean +++ b/src/algebra/continued_fractions/computation/basic.lean @@ -5,7 +5,7 @@ Authors: Kevin Kappelmann -/ import algebra.order.floor import algebra.continued_fractions.basic -import algebra.order.field +import algebra.order.field.basic /-! # Computable Continued Fractions diff --git a/src/algebra/order/absolute_value.lean b/src/algebra/order/absolute_value.lean index 3bfce7120fe8a..ce9610ba3d535 100644 --- a/src/algebra/order/absolute_value.lean +++ b/src/algebra/order/absolute_value.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Anne Baanen. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Anne Baanen -/ -import algebra.order.field +import algebra.order.field.basic import algebra.order.hom.basic /-! diff --git a/src/algebra/order/field.lean b/src/algebra/order/field/basic.lean similarity index 98% rename from src/algebra/order/field.lean rename to src/algebra/order/field/basic.lean index 85b3a72e45127..8c3252e6d4415 100644 --- a/src/algebra/order/field.lean +++ b/src/algebra/order/field/basic.lean @@ -3,9 +3,8 @@ Copyright (c) 2014 Robert Lewis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn -/ -import algebra.order.field_defs -import algebra.order.with_zero -import data.fintype.basic +import algebra.order.field.defs +import algebra.group_with_zero.power /-! # Linear ordered (semi)fields @@ -635,19 +634,6 @@ lemma is_glb.mul_right {s : set α} (ha : 0 ≤ a) (hs : is_glb s b) : is_glb ((λ b, b * a) '' s) (b * a) := by simpa [mul_comm] using hs.mul_left ha -lemma pi.exists_forall_pos_add_lt [has_exists_add_of_le α] [finite ι] {x y : ι → α} - (h : ∀ i, x i < y i) : ∃ ε, 0 < ε ∧ ∀ i, x i + ε < y i := -begin - casesI nonempty_fintype ι, - casesI is_empty_or_nonempty ι, - { exact ⟨1, zero_lt_one, is_empty_elim⟩ }, - choose ε hε hxε using λ 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 (λ i _, hε _), - exact ⟨_, half_pos hε, λ i, add_lt_add_left ((half_lt_self hε).trans_le $ finset.inf'_le _ $ - finset.mem_univ _) _⟩, -end - end linear_ordered_semifield section diff --git a/src/algebra/order/field_defs.lean b/src/algebra/order/field/defs.lean similarity index 98% rename from src/algebra/order/field_defs.lean rename to src/algebra/order/field/defs.lean index 3dd6d4e002a97..57d0fc760dc02 100644 --- a/src/algebra/order/field_defs.lean +++ b/src/algebra/order/field/defs.lean @@ -21,7 +21,7 @@ A linear ordered (semi)field is a (semi)field equipped with a linear order such ## Implementation details -For olean caching reasons, this file is separate to the main file, algebra.order.field. +For olean caching reasons, this file is separate to the main file, `algebra.order.field.basic`. The lemmata are instead located there. -/ diff --git a/src/algebra/order/field/pi.lean b/src/algebra/order/field/pi.lean new file mode 100644 index 0000000000000..ff6616f40178e --- /dev/null +++ b/src/algebra/order/field/pi.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2014 Robert Lewis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yaël Dillies +-/ +import algebra.order.field.basic +import data.fintype.basic + +/-! +# Lemmas about (finite domain) functions into fields. + +We split this from `algebra.order.field.basic` to avoid importing the finiteness hierarchy there. +-/ + +variables {α ι : Type*} [linear_ordered_semifield α] + +lemma pi.exists_forall_pos_add_lt [has_exists_add_of_le α] [finite ι] {x y : ι → α} + (h : ∀ i, x i < y i) : ∃ ε, 0 < ε ∧ ∀ i, x i + ε < y i := +begin + casesI nonempty_fintype ι, + casesI is_empty_or_nonempty ι, + { exact ⟨1, zero_lt_one, is_empty_elim⟩ }, + choose ε hε hxε using λ 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 (λ i _, hε _), + exact ⟨_, half_pos hε, λ i, add_lt_add_left ((half_lt_self hε).trans_le $ finset.inf'_le _ $ + finset.mem_univ _) _⟩, +end diff --git a/src/algebra/order/positive/field.lean b/src/algebra/order/positive/field.lean index ea8e3f6f66f01..1f17bb920c68b 100644 --- a/src/algebra/order/positive/field.lean +++ b/src/algebra/order/positive/field.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ -import algebra.order.field +import algebra.order.field.basic import algebra.order.positive.ring /-! diff --git a/src/algebra/order/smul.lean b/src/algebra/order/smul.lean index fee091ad4cbd3..3662e67bcf030 100644 --- a/src/algebra/order/smul.lean +++ b/src/algebra/order/smul.lean @@ -5,7 +5,7 @@ Authors: Frédéric Dupuis -/ import algebra.module.pi import algebra.module.prod -import algebra.order.field +import algebra.order.field.basic import algebra.order.pi import data.set.pointwise.basic import tactic.positivity diff --git a/src/analysis/special_functions/bernstein.lean b/src/analysis/special_functions/bernstein.lean index f7532b07c6960..85c7711ca68c8 100644 --- a/src/analysis/special_functions/bernstein.lean +++ b/src/analysis/special_functions/bernstein.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ -import algebra.order.field +import algebra.order.field.basic import ring_theory.polynomial.bernstein import topology.continuous_function.polynomial diff --git a/src/analysis/specific_limits/normed.lean b/src/analysis/specific_limits/normed.lean index 07aa0f37e9d40..14ce7e45cac43 100644 --- a/src/analysis/specific_limits/normed.lean +++ b/src/analysis/specific_limits/normed.lean @@ -3,7 +3,7 @@ Copyright (c) 2020 Sébastien Gouëzel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Anatole Dedecker, Sébastien Gouëzel, Yury G. Kudryashov, Dylan MacKenzie, Patrick Massot -/ -import algebra.order.field +import algebra.order.field.basic import analysis.asymptotics.asymptotics import analysis.specific_limits.basic diff --git a/src/data/nat/cast_field.lean b/src/data/nat/cast_field.lean index 756844efebfc6..15383ed744c93 100644 --- a/src/data/nat/cast_field.lean +++ b/src/data/nat/cast_field.lean @@ -3,7 +3,7 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Yaël Dillies, Patrick Stevens -/ -import algebra.order.field +import algebra.order.field.basic import data.nat.cast /-! diff --git a/src/data/nat/choose/bounds.lean b/src/data/nat/choose/bounds.lean index 113353b97d516..b20b776752edb 100644 --- a/src/data/nat/choose/bounds.lean +++ b/src/data/nat/choose/bounds.lean @@ -5,7 +5,7 @@ Authors: Yaël Dillies, Eric Rodriguez -/ import algebra.group_power.lemmas -import algebra.order.field +import algebra.order.field.basic import data.nat.cast import data.nat.choose.basic diff --git a/src/data/rat/order.lean b/src/data/rat/order.lean index 2157df0da1cf0..506112491ee7f 100644 --- a/src/data/rat/order.lean +++ b/src/data/rat/order.lean @@ -3,7 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Mario Carneiro -/ -import algebra.order.field +import algebra.order.field.basic import data.rat.basic /-! diff --git a/src/data/set/intervals/image_preimage.lean b/src/data/set/intervals/image_preimage.lean index 70f285b5a8a24..12de3d9947f87 100644 --- a/src/data/set/intervals/image_preimage.lean +++ b/src/data/set/intervals/image_preimage.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury G. Kudryashov, Patrick Massot -/ import data.set.pointwise.basic -import algebra.order.field +import algebra.order.field.basic /-! # (Pre)images of intervals diff --git a/src/order/filter/at_top_bot.lean b/src/order/filter/at_top_bot.lean index d473d68e67169..729fe4138614d 100644 --- a/src/order/filter/at_top_bot.lean +++ b/src/order/filter/at_top_bot.lean @@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov, Patrick Massot -/ -import algebra.order.field +import algebra.order.field.basic import data.finset.preimage import data.set.intervals.disjoint import order.filter.bases