Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 1f0096e

Browse files
urkudurkud
committed
refactor(data/set/finite): reduce imports (#18245)
* Add `eq_or_eq_or_eq_of_forall_not_lt_lt`, `finite.of_forall_not_lt_lt`, `set.finite_of_forall_not_lt_lt` (replacing `set.finite_of_forall_between_eq_endpoints`), and `set.finite_of_forall_not_lt_lt'`. * Import `data.finset.basic` instead of `data.finset.sort` in `data.set.finite`. * Forward-ported in leanprover-community/mathlib4#1738
1 parent 160ef3e commit 1f0096e

5 files changed

Lines changed: 37 additions & 40 deletions

File tree

‎src/data/polynomial/basic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
55
-/
66
import algebra.monoid_algebra.basic
7+
import data.finset.sort
78

89
/-!
910
# Theory of univariate polynomials

‎src/data/set/finite.lean‎

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl, Mario Carneiro, Kyle Miller
55
-/
6-
import data.finset.sort
6+
import data.finset.basic
77
import data.set.functor
88
import data.finite.basic
99

@@ -1227,27 +1227,27 @@ s.finite_to_set.bdd_below
12271227

12281228
end finset
12291229

1230-
/--
1231-
If a set `s` does not contain any elements between any pair of elements `x, z ∈ s` with `x ≤ z`
1232-
(i.e if given `x, y, z ∈ s` such that `x ≤ y ≤ z`, then `y` is either `x` or `z`), then `s` is
1233-
finite.
1234-
-/
1235-
lemma set.finite_of_forall_between_eq_endpoints {α : Type*} [linear_order α] (s : set α)
1236-
(h : ∀ (x ∈ s) (y ∈ s) (z ∈ s), x ≤ y → y ≤ z → x = y ∨ y = z) :
1237-
set.finite s :=
1230+
variables [linear_order α]
1231+
1232+
/-- If a linear order does not contain any triple of elements `x < y < z`, then this type
1233+
is finite. -/
1234+
lemma finite.of_forall_not_lt_lt (h : ∀ ⦃x y z : α⦄, x < y → y < z → false) :
1235+
finite α :=
12381236
begin
1239-
by_contra hinf,
1240-
change s.infinite at hinf,
1241-
rcases hinf.exists_subset_card_eq 3 with ⟨t, hts, ht⟩,
1242-
let f := t.order_iso_of_fin ht,
1243-
let x := f 0,
1244-
let y := f 1,
1245-
let z := f 2,
1246-
have := h x (hts x.2) y (hts y.2) z (hts z.2)
1247-
(f.monotone $ by dec_trivial) (f.monotone $ by dec_trivial),
1248-
have key₁ : (0 : fin 3) ≠ 1 := by dec_trivial,
1249-
have key₂ : (1 : fin 3) ≠ 2 := by dec_trivial,
1250-
cases this,
1251-
{ dsimp only [x, y] at this, exact key₁ (f.injective $ subtype.coe_injective this) },
1252-
{ dsimp only [y, z] at this, exact key₂ (f.injective $ subtype.coe_injective this) }
1237+
nontriviality α,
1238+
rcases exists_pair_ne α with ⟨x, y, hne⟩,
1239+
refine @finite.of_fintype α ⟨{x, y}, λ z , _⟩,
1240+
simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y
12531241
end
1242+
1243+
/-- If a set `s` does not contain any triple of elements `x < y < z`, then `s` is finite. -/
1244+
lemma set.finite_of_forall_not_lt_lt {s : set α} (h : ∀ (x y z ∈ s), x < y → y < z → false) :
1245+
set.finite s :=
1246+
@set.to_finite _ s $ finite.of_forall_not_lt_lt $ by simpa only [set_coe.forall'] using h
1247+
1248+
lemma set.finite_diff_Union_Ioo (s : set α) : (s \ ⋃ (x ∈ s) (y ∈ s), Ioo x y).finite :=
1249+
set.finite_of_forall_not_lt_lt $ λ x hx y hy z hz hxy hyz, hy.2 $ mem_Union₂_of_mem hx.1 $
1250+
mem_Union₂_of_mem hz.1 ⟨hxy, hyz⟩
1251+
1252+
lemma set.finite_diff_Union_Ioo' (s : set α) : (s \ ⋃ x : s × s, Ioo x.1 x.2).finite :=
1253+
by simpa only [Union, supr_prod, supr_subtype] using s.finite_diff_Union_Ioo

‎src/measure_theory/constructions/borel_space.lean‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -485,11 +485,7 @@ begin
485485
let u := ⋃ (x ∈ s) (y ∈ s), Ioo x y,
486486
have huopen : is_open u := is_open_bUnion (λ x hx, is_open_bUnion (λ y hy, is_open_Ioo)),
487487
have humeas : measurable_set u := huopen.measurable_set,
488-
have hfinite : (s \ u).finite,
489-
{ refine set.finite_of_forall_between_eq_endpoints (s \ u) (λ x hx y hy z hz hxy hyz, _),
490-
by_contra' h,
491-
exact hy.2 (mem_Union₂.mpr ⟨x, hx.1,
492-
mem_Union₂.mpr ⟨z, hz.1, lt_of_le_of_ne hxy h.1, lt_of_le_of_ne hyz h.2⟩⟩) },
488+
have hfinite : (s \ u).finite := s.finite_diff_Union_Ioo,
493489
have : u ⊆ s :=
494490
Union₂_subset (λ x hx, Union₂_subset (λ y hy, Ioo_subset_Icc_self.trans (h.out hx hy))),
495491
rw ← union_diff_cancel this,

‎src/measure_theory/measure/lebesgue.lean‎

Lines changed: 2 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -542,12 +542,7 @@ begin
542542
two endpoints, which don't matter since `μ` does not have any atom). -/
543543
let T : s × s → set ℝ := λ p, Ioo p.1 p.2,
544544
let u := ⋃ (i : ↥s × ↥s), T i,
545-
have hfinite : (s \ u).finite,
546-
{ refine set.finite_of_forall_between_eq_endpoints (s \ u) (λ x hx y hy z hz hxy hyz, _),
547-
by_contra' h,
548-
apply hy.2,
549-
exact mem_Union_of_mem (⟨x, hx.1⟩, ⟨z, hz.1⟩)
550-
⟨lt_of_le_of_ne hxy h.1, lt_of_le_of_ne hyz h.2⟩ },
545+
have hfinite : (s \ u).finite := s.finite_diff_Union_Ioo',
551546
obtain ⟨A, A_count, hA⟩ :
552547
∃ (A : set (↥s × ↥s)), A.countable ∧ (⋃ (i ∈ A), T i) = ⋃ (i : ↥s × ↥s), T i :=
553548
is_open_Union_countable _ (λ p, is_open_Ioo),
@@ -584,12 +579,7 @@ begin
584579
two endpoints, which don't matter since `μ` does not have any atom). -/
585580
let T : s × s → set ℝ := λ p, Ioo p.1 p.2,
586581
let u := ⋃ (i : ↥s × ↥s), T i,
587-
have hfinite : (s \ u).finite,
588-
{ refine set.finite_of_forall_between_eq_endpoints (s \ u) (λ x hx y hy z hz hxy hyz, _),
589-
by_contra' h,
590-
apply hy.2,
591-
exact mem_Union_of_mem (⟨x, hx.1⟩, ⟨z, hz.1⟩)
592-
⟨lt_of_le_of_ne hxy h.1, lt_of_le_of_ne hyz h.2⟩ },
582+
have hfinite : (s \ u).finite := s.finite_diff_Union_Ioo',
593583
obtain ⟨A, A_count, hA⟩ :
594584
∃ (A : set (↥s × ↥s)), A.countable ∧ (⋃ (i ∈ A), T i) = ⋃ (i : ↥s × ↥s), T i :=
595585
is_open_Union_countable _ (λ p, is_open_Ioo),

‎src/order/basic.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -876,6 +876,16 @@ or_iff_not_imp_left.2 $ λ h,
876876
⟨λ a ha₁, le_of_not_gt $ λ ha₂, h ⟨a, ha₁, ha₂⟩,
877877
λ a ha₂, le_of_not_gt $ λ ha₁, h ⟨a, ha₁, ha₂⟩⟩
878878

879+
/-- If a linear order has no elements `x < y < z`, then it has at most two elements. -/
880+
lemma eq_or_eq_or_eq_of_forall_not_lt_lt {α : Type*} [linear_order α]
881+
(h : ∀ ⦃x y z : α⦄, x < y → y < z → false) (x y z : α) : x = y ∨ y = z ∨ x = z :=
882+
begin
883+
by_contra hne, push_neg at hne,
884+
cases hne.1.lt_or_lt with h₁ h₁; cases hne.2.1.lt_or_lt with h₂ h₂;
885+
cases hne.2.2.lt_or_lt with h₃ h₃,
886+
exacts [h h₁ h₂, h h₂ h₃, h h₃ h₂, h h₃ h₁, h h₁ h₃, h h₂ h₃, h h₁ h₃, h h₂ h₁]
887+
end
888+
879889
namespace punit
880890
variables (a b : punit.{u+1})
881891

0 commit comments

Comments
 (0)