From 328375597f2c0dd00522d9c2e5a33b6a6128feeb Mon Sep 17 00:00:00 2001 From: damiano Date: Tue, 30 May 2023 23:18:13 +0000 Subject: [PATCH] chore(archive + counterexamples): namespaces imo, theorems_100, counterexample, plus three more (#19129) This PR is a revision of #19122: it addresses namespacing in `archive` and `counterexamples`. The main difference with #19122 is that it adds namespaces less aggressively: I added a namespace only if there was not an explicit namespace after the initial "fluff". In `counterexamples`, I added namespaces to all files. I introduced three "main" namespaces: `imo, theorems_100, counterexample` (the last one singular). Besides these, I also introduced the namespaces `prop_encodable, oxford_invariants, sensitivity`, to cover the left-over files in `archive`. Note that if a file has `namespace` early on, then it does not get a new namespace, even though it might be desirable for it to have one. Comments are very welcome! Note: besides adding namespaces, the only files that I had to manually edit are the ones in * commit d337b99e3e6d147d440c91874d1809a3ee04ff16 -- I do not like these changes, but currently do not see how to avoid them; * commit 48471f35ec9f9929dd35363ee176f8c889042f6e -- I *removed* an pre-existing namespace, replacing it by `open `. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mk_all.2Esh): this PR is motivated by the desire to port to mathlib4 the files in `archive, counterexamples`, taking advantage of `mathport`. The namespacing helps with avoiding clashes among names of declarations, as well as one-lettered declarations in the root namespace. --- .../37_solution_of_cubic.lean | 4 +++ .../42_inverse_triangle_sum.lean | 2 +- archive/100-theorems-list/45_partition.lean | 4 +++ .../100-theorems-list/57_herons_formula.lean | 4 +++ .../100-theorems-list/70_perfect_numbers.lean | 33 +++++++++++-------- .../73_ascending_descending_sequences.lean | 4 +++ .../81_sum_of_prime_reciprocals_diverges.lean | 4 +++ .../100-theorems-list/82_cubing_a_cube.lean | 4 +++ .../83_friendship_graphs.lean | 6 +++- .../93_birthday_problem.lean | 4 +++ .../100-theorems-list/9_area_of_a_circle.lean | 4 +++ archive/examples/prop_encodable.lean | 4 +++ archive/imo/imo1959_q1.lean | 4 +++ archive/imo/imo1962_q4.lean | 4 +++ archive/imo/imo1972_q5.lean | 4 +++ archive/imo/imo1975_q1.lean | 4 +++ archive/imo/imo1977_q6.lean | 4 +++ archive/imo/imo1988_q6.lean | 4 +++ archive/imo/imo1994_q1.lean | 4 +++ archive/imo/imo1998_q2.lean | 4 +++ archive/imo/imo2001_q2.lean | 4 +++ archive/imo/imo2001_q6.lean | 4 +++ archive/imo/imo2005_q3.lean | 4 +++ archive/imo/imo2005_q4.lean | 4 +++ archive/imo/imo2006_q3.lean | 4 +++ archive/imo/imo2006_q5.lean | 4 +++ archive/imo/imo2008_q2.lean | 4 +++ archive/imo/imo2008_q3.lean | 4 +++ archive/imo/imo2008_q4.lean | 4 +++ archive/imo/imo2011_q3.lean | 4 +++ archive/imo/imo2011_q5.lean | 4 +++ archive/imo/imo2013_q1.lean | 4 +++ archive/imo/imo2013_q5.lean | 4 +++ archive/imo/imo2019_q1.lean | 4 +++ archive/imo/imo2019_q2.lean | 4 +++ archive/imo/imo2019_q4.lean | 4 +++ archive/imo/imo2020_q2.lean | 4 +++ archive/imo/imo2021_q1.lean | 4 +++ .../2021summer/week3_p1.lean | 2 +- archive/sensitivity.lean | 4 +++ ...nically_ordered_comm_semiring_two_mul.lean | 4 +++ counterexamples/char_p_zero_ne_char_zero.lean | 4 +++ counterexamples/cyclotomic_105.lean | 4 +++ counterexamples/direct_sum_is_internal.lean | 4 +++ counterexamples/girard.lean | 4 +++ .../homogeneous_prime_not_prime.lean | 4 +++ ...linear_order_with_pos_mul_pos_eq_zero.lean | 4 +++ counterexamples/map_floor.lean | 4 +++ counterexamples/phillips.lean | 4 +++ counterexamples/pseudoelement.lean | 6 ++-- counterexamples/quadratic_form.lean | 4 +++ .../seminorm_lattice_not_distrib.lean | 4 +++ counterexamples/sorgenfrey_line.lean | 4 +++ .../zero_divisors_in_add_monoid_algebras.lean | 4 +++ 54 files changed, 226 insertions(+), 19 deletions(-) diff --git a/archive/100-theorems-list/37_solution_of_cubic.lean b/archive/100-theorems-list/37_solution_of_cubic.lean index aca8b61c940bc..8c5c11284e4e6 100644 --- a/archive/100-theorems-list/37_solution_of_cubic.lean +++ b/archive/100-theorems-list/37_solution_of_cubic.lean @@ -35,6 +35,8 @@ Originally ported from Isabelle/HOL. The polynomial, cubic, root -/ +namespace theorems_100 + section field open polynomial @@ -184,3 +186,5 @@ begin end end field + +end theorems_100 diff --git a/archive/100-theorems-list/42_inverse_triangle_sum.lean b/archive/100-theorems-list/42_inverse_triangle_sum.lean index 063c4d35bf0b7..0b12999fbf3d8 100644 --- a/archive/100-theorems-list/42_inverse_triangle_sum.lean +++ b/archive/100-theorems-list/42_inverse_triangle_sum.lean @@ -23,7 +23,7 @@ open_locale big_operators open finset /-- **Sum of the Reciprocals of the Triangular Numbers** -/ -lemma inverse_triangle_sum : +lemma theorem_100.inverse_triangle_sum : ∀ n, ∑ k in range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n := begin refine sum_range_induction _ _ (if_pos rfl) _, diff --git a/archive/100-theorems-list/45_partition.lean b/archive/100-theorems-list/45_partition.lean index 0fe42d3f7c6f1..8796e3b3c2a4d 100644 --- a/archive/100-theorems-list/45_partition.lean +++ b/archive/100-theorems-list/45_partition.lean @@ -53,6 +53,8 @@ https://en.wikipedia.org/wiki/Partition_(number_theory)#Odd_parts_and_distinct_p -/ open power_series +namespace theorems_100 + noncomputable theory variables {α : Type*} @@ -521,3 +523,5 @@ begin rw odd_gf_prop n (n+1) (by linarith), apply same_coeffs (n+1) n n.le_succ, end + +end theorems_100 diff --git a/archive/100-theorems-list/57_herons_formula.lean b/archive/100-theorems-list/57_herons_formula.lean index 7d288df537ac0..100102469b88c 100644 --- a/archive/100-theorems-list/57_herons_formula.lean +++ b/archive/100-theorems-list/57_herons_formula.lean @@ -21,6 +21,8 @@ lengths. open real euclidean_geometry open_locale real euclidean_geometry +namespace theorems_100 + local notation `√` := real.sqrt variables {V : Type*} {P : Type*} @@ -61,3 +63,5 @@ begin one_mul, mul_div_cancel]; norm_num, end + +end theorems_100 diff --git a/archive/100-theorems-list/70_perfect_numbers.lean b/archive/100-theorems-list/70_perfect_numbers.lean index 69804193d4e8d..7d1cbd45655a7 100644 --- a/archive/100-theorems-list/70_perfect_numbers.lean +++ b/archive/100-theorems-list/70_perfect_numbers.lean @@ -26,21 +26,23 @@ Euler proved the converse, that if `n` is even and perfect, then there exists `k https://en.wikipedia.org/wiki/Euclid%E2%80%93Euler_theorem -/ +namespace theorems_100 + lemma odd_mersenne_succ (k : ℕ) : ¬ 2 ∣ mersenne (k + 1) := by simp [← even_iff_two_dvd, ← nat.even_add_one] with parity_simps namespace nat -open arithmetic_function finset +open nat.arithmetic_function finset open_locale arithmetic_function lemma sigma_two_pow_eq_mersenne_succ (k : ℕ) : σ 1 (2 ^ k) = mersenne (k + 1) := -by simp [sigma_one_apply, mersenne, prime_two, ← geom_sum_mul_add 1 (k+1)] +by simp [sigma_one_apply, mersenne, nat.prime_two, ← geom_sum_mul_add 1 (k+1)] /-- Euclid's theorem that Mersenne primes induce perfect numbers -/ theorem perfect_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).prime) : - perfect ((2 ^ k) * mersenne (k + 1)) := + nat.perfect ((2 ^ k) * mersenne (k + 1)) := begin - rw [perfect_iff_sum_divisors_eq_two_mul, ← mul_assoc, ← pow_succ, ← sigma_one_apply, mul_comm, + rw [nat.perfect_iff_sum_divisors_eq_two_mul, ← mul_assoc, ← pow_succ, ← sigma_one_apply, mul_comm, is_multiplicative_sigma.map_mul_of_coprime (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)), sigma_two_pow_eq_mersenne_succ], @@ -53,7 +55,7 @@ lemma ne_zero_of_prime_mersenne (k : ℕ) (pr : (mersenne (k + 1)).prime) : k ≠ 0 := begin intro H, - simpa [H, mersenne, not_prime_one] using pr, + simpa [H, mersenne, nat.not_prime_one] using pr, end theorem even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).prime) : @@ -77,26 +79,26 @@ end /-- **Perfect Number Theorem**: Euler's theorem that even perfect numbers can be factored as a power of two times a Mersenne prime. -/ -theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : even n) (perf : perfect n) : - ∃ (k : ℕ), prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) := +theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : even n) (perf : nat.perfect n) : + ∃ (k : ℕ), nat.prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) := begin have hpos := perf.2, rcases eq_two_pow_mul_odd hpos with ⟨k, m, rfl, hm⟩, use k, rw even_iff_two_dvd at hm, - rw [perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply, + rw [nat.perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply, is_multiplicative_sigma.map_mul_of_coprime (nat.prime_two.coprime_pow_of_not_dvd hm).symm, sigma_two_pow_eq_mersenne_succ, ← mul_assoc, ← pow_succ] at perf, rcases nat.coprime.dvd_of_dvd_mul_left (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)) (dvd.intro _ perf) with ⟨j, rfl⟩, rw [← mul_assoc, mul_comm _ (mersenne _), mul_assoc] at perf, have h := mul_left_cancel₀ (ne_of_gt (mersenne_pos (nat.succ_pos _))) perf, - rw [sigma_one_apply, sum_divisors_eq_sum_proper_divisors_add_self, ← succ_mersenne, add_mul, + rw [sigma_one_apply, nat.sum_divisors_eq_sum_proper_divisors_add_self, ← succ_mersenne, add_mul, one_mul, add_comm] at h, have hj := add_left_cancel h, - cases sum_proper_divisors_dvd (by { rw hj, apply dvd.intro_left (mersenne (k + 1)) rfl }), + cases nat.sum_proper_divisors_dvd (by { rw hj, apply dvd.intro_left (mersenne (k + 1)) rfl }), { have j1 : j = 1 := eq.trans hj.symm h_1, - rw [j1, mul_one, sum_proper_divisors_eq_one_iff_prime] at h_1, + rw [j1, mul_one, nat.sum_proper_divisors_eq_one_iff_prime] at h_1, simp [h_1, j1] }, { have jcon := eq.trans hj.symm h_1, rw [← one_mul j, ← mul_assoc, mul_one] at jcon, @@ -108,7 +110,7 @@ begin rw [← jcon2, one_mul], exact even_iff_two_dvd.mp ev }, apply ne_of_lt _ jcon2, - rw [mersenne, ← nat.pred_eq_sub_one, lt_pred_iff, ← pow_one (nat.succ 1)], + rw [mersenne, ← nat.pred_eq_sub_one, nat.lt_pred_iff, ← pow_one (nat.succ 1)], apply pow_lt_pow (nat.lt_succ_self 1) (nat.succ_lt_succ (nat.succ_pos k)) }, contrapose! hm, simp [hm] } @@ -116,13 +118,16 @@ end /-- The Euclid-Euler theorem characterizing even perfect numbers -/ theorem even_and_perfect_iff {n : ℕ} : - (even n ∧ perfect n) ↔ ∃ (k : ℕ), prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) := + (even n ∧ nat.perfect n) ↔ + ∃ (k : ℕ), nat.prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) := begin split, { rintro ⟨ev, perf⟩, - exact eq_two_pow_mul_prime_mersenne_of_even_perfect ev perf }, + exact nat.eq_two_pow_mul_prime_mersenne_of_even_perfect ev perf }, { rintro ⟨k, pr, rfl⟩, exact ⟨even_two_pow_mul_mersenne_of_prime k pr, perfect_two_pow_mul_mersenne_of_prime k pr⟩ } end end nat + +end theorems_100 diff --git a/archive/100-theorems-list/73_ascending_descending_sequences.lean b/archive/100-theorems-list/73_ascending_descending_sequences.lean index ce47545e5e0c2..2c2d3931d8d69 100644 --- a/archive/100-theorems-list/73_ascending_descending_sequences.lean +++ b/archive/100-theorems-list/73_ascending_descending_sequences.lean @@ -26,6 +26,8 @@ variables {α : Type*} [linear_order α] {β : Type*} open function finset open_locale classical +namespace theorems_100 + /-- **Erdős–Szekeres Theorem**: Given a sequence of more than `r * s` distinct values, there is an increasing sequence of length longer than `r` or a decreasing sequence of length longer than `s`. @@ -158,3 +160,5 @@ begin -- Which follows from considering the cardinalities of the subset above, since `ab` is injective. simpa [nat.succ_injective, card_image_of_injective, ‹injective ab›] using card_le_of_subset this, end + +end theorems_100 diff --git a/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean b/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean index a07a1d585cafc..062c3d870d2d6 100644 --- a/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean +++ b/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean @@ -42,6 +42,8 @@ open_locale big_operators open_locale classical open filter finset +namespace theorems_100 + /-- The primes in `(k, x]`. -/ @@ -246,3 +248,5 @@ begin ... < x / 2 + x / 2 : add_lt_add_of_lt_of_le h3 h4 ... = x : add_halves ↑x, end + +end theorems_100 diff --git a/archive/100-theorems-list/82_cubing_a_cube.lean b/archive/100-theorems-list/82_cubing_a_cube.lean index 62061c0d53a07..ab4b567df3ac4 100644 --- a/archive/100-theorems-list/82_cubing_a_cube.lean +++ b/archive/100-theorems-list/82_cubing_a_cube.lean @@ -18,6 +18,8 @@ http://www.alaricstephen.com/main-featured/2017/9/28/cubing-a-cube-proof open real set function fin +namespace theorems_100 + noncomputable theory namespace «82» @@ -520,3 +522,5 @@ begin end end «82» + +end theorems_100 diff --git a/archive/100-theorems-list/83_friendship_graphs.lean b/archive/100-theorems-list/83_friendship_graphs.lean index a60e1e69bdf6a..adf5f345655a9 100644 --- a/archive/100-theorems-list/83_friendship_graphs.lean +++ b/archive/100-theorems-list/83_friendship_graphs.lean @@ -39,6 +39,8 @@ be phrased in terms of counting walks. -/ open_locale classical big_operators +namespace theorems_100 + noncomputable theory open finset simple_graph matrix @@ -144,7 +146,7 @@ begin use G.degree v, intro x, by_cases hvx : G.adj v x, swap, { exact (degree_eq_of_not_adj hG hvx).symm, }, - dunfold exists_politician at hG', + dunfold theorems_100.exists_politician at hG', push_neg at hG', rcases hG' v with ⟨w, hvw', hvw⟩, rcases hG' x with ⟨y, hxy', hxy⟩, @@ -336,3 +338,5 @@ begin { exact npG (hG.exists_politician_of_degree_le_two dreg (nat.lt_succ_iff.mp dle2)) }, { exact hG.false_of_three_le_degree dreg dge3 }, end + +end theorems_100 diff --git a/archive/100-theorems-list/93_birthday_problem.lean b/archive/100-theorems-list/93_birthday_problem.lean index 6d9c2d8bf3b1d..d4544a61f7f70 100644 --- a/archive/100-theorems-list/93_birthday_problem.lean +++ b/archive/100-theorems-list/93_birthday_problem.lean @@ -17,6 +17,8 @@ in terms of injective functions. The general result about `fintype.card (α ↪ uses is `fintype.card_embedding_eq`. -/ +namespace theorems_100 + local notation (name := finset.card) `|` x `|` := finset.card x local notation (name := fintype.card) `‖` x `‖` := fintype.card x @@ -75,3 +77,5 @@ begin end end measure_theory + +end theorems_100 diff --git a/archive/100-theorems-list/9_area_of_a_circle.lean b/archive/100-theorems-list/9_area_of_a_circle.lean index 76a34c96e6023..e3c8d7a0daf6f 100644 --- a/archive/100-theorems-list/9_area_of_a_circle.lean +++ b/archive/100-theorems-list/9_area_of_a_circle.lean @@ -43,6 +43,8 @@ to the n-ball. open set real measure_theory interval_integral open_locale real nnreal +namespace theorems_100 + /-- A disc of radius `r` is defined as the collection of points `(p.1, p.2)` in `ℝ × ℝ` such that `p.1 ^ 2 + p.2 ^ 2 < r ^ 2`. Note that this definition is not equivalent to `metric.ball (0 : ℝ × ℝ) r`. This was done @@ -115,3 +117,5 @@ begin hcont hderiv (continuous_const.mul hf).continuous_on.interval_integrable ... = nnreal.pi * r ^ 2 : by norm_num [F, inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π], end + +end theorems_100 diff --git a/archive/examples/prop_encodable.lean b/archive/examples/prop_encodable.lean index 4890ca2837d89..a877eeed41334 100644 --- a/archive/examples/prop_encodable.lean +++ b/archive/examples/prop_encodable.lean @@ -24,6 +24,8 @@ We mark the auxiliary constructions `private`, since their only purpose is to show encodability. -/ +namespace prop_encodable + /-- Propositional formulas with labels from `α`. -/ inductive prop_form (α : Type*) | var : α → prop_form @@ -96,3 +98,5 @@ begin end end prop_form + +end prop_encodable diff --git a/archive/imo/imo1959_q1.lean b/archive/imo/imo1959_q1.lean index 750f25078a713..b1af08fd9b9fa 100644 --- a/archive/imo/imo1959_q1.lean +++ b/archive/imo/imo1959_q1.lean @@ -18,6 +18,8 @@ as saying the numerator and denominator are relatively prime. open nat +namespace imo + lemma calculation (n k : ℕ) (h1 : k ∣ 21 * n + 4) (h2 : k ∣ 14 * n + 3) : k ∣ 1 := have h3 : k ∣ 2 * (21 * n + 4), from h1.mul_left 2, have h4 : k ∣ 3 * (14 * n + 3), from h2.mul_left 3, @@ -26,3 +28,5 @@ have h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1, by ring, theorem imo1959_q1 : ∀ n : ℕ, coprime (21 * n + 4) (14 * n + 3) := assume n, coprime_of_dvd' $ λ k hp h1 h2, calculation n k h1 h2 + +end imo diff --git a/archive/imo/imo1962_q4.lean b/archive/imo/imo1962_q4.lean index 42bf061c48fb1..65b534aba58e9 100644 --- a/archive/imo/imo1962_q4.lean +++ b/archive/imo/imo1962_q4.lean @@ -17,6 +17,8 @@ in fact the simplest form of the set of solutions, and then prove it equals the open real open_locale real +namespace imo + noncomputable theory def problem_equation (x : ℝ) : Prop := cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1 @@ -129,3 +131,5 @@ calc problem_equation x ↔ cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1 : by refl ... ↔ cos (2 * x) = 0 ∨ cos (3 * x) = 0 : by simp [cos_two_mul, cos_three_mul, formula] ... ↔ x ∈ solution_set : by { rw [solve_cos2x_0, solve_cos3x_0, ← exists_or_distrib], refl } + +end imo diff --git a/archive/imo/imo1972_q5.lean b/archive/imo/imo1972_q5.lean index 21178464e58dd..27b0e32c8e3f0 100644 --- a/archive/imo/imo1972_q5.lean +++ b/archive/imo/imo1972_q5.lean @@ -15,6 +15,8 @@ Problem: `f` and `g` are real-valued functions defined on the real line. For all Prove that `|g(x)| ≤ 1` for all `x`. -/ +namespace imo + /-- This proof begins by introducing the supremum of `f`, `k ≤ 1` as well as `k' = k / ‖g y‖`. We then suppose that the conclusion does not hold (`hneg`) and show that `k ≤ k'` (by @@ -120,3 +122,5 @@ begin ... ≤ 2 * k : by linarith [h (x+y), h (x -y)] }, linarith, end + +end imo diff --git a/archive/imo/imo1975_q1.lean b/archive/imo/imo1975_q1.lean index 47170ea79e550..43a6e9409a65b 100644 --- a/archive/imo/imo1975_q1.lean +++ b/archive/imo/imo1975_q1.lean @@ -31,6 +31,8 @@ variables (hx : antitone_on x (finset.Icc 1 n)) variables (hy : antitone_on y (finset.Icc 1 n)) include hx hy hσ +namespace imo + theorem IMO_1975_Q1 : ∑ i in finset.Icc 1 n, (x i - y i) ^ 2 ≤ ∑ i in finset.Icc 1 n, (x i - y (σ i)) ^ 2 := begin @@ -46,3 +48,5 @@ begin -- them being `decreasing` exact antitone_on.monovary_on hx hy end + +end imo diff --git a/archive/imo/imo1977_q6.lean b/archive/imo/imo1977_q6.lean index 1c65f6af0c855..79342518718c7 100644 --- a/archive/imo/imo1977_q6.lean +++ b/archive/imo/imo1977_q6.lean @@ -15,6 +15,8 @@ We first prove the problem statement for `f : ℕ → ℕ` then we use it to prove the statement for positive naturals. -/ +namespace imo + theorem imo1977_q6_nat (f : ℕ → ℕ) (h : ∀ n, f (f n) < f (n + 1)) : ∀ n, f n = n := begin @@ -42,3 +44,5 @@ begin { simp }, { simpa using h _ } } end + +end imo diff --git a/archive/imo/imo1988_q6.lean b/archive/imo/imo1988_q6.lean index 044358ba8f7bd..8913a0c8dc30a 100644 --- a/archive/imo/imo1988_q6.lean +++ b/archive/imo/imo1988_q6.lean @@ -25,6 +25,8 @@ To illustrate the technique, we also prove a similar result. -- open_locale classical +namespace imo + local attribute [instance] classical.prop_decidable local attribute [simp] sq @@ -296,3 +298,5 @@ begin obtain rfl|rfl := (nat.dvd_prime nat.prime_two).mp y_dvd; apply mul_left_cancel₀, exacts [one_ne_zero, h.symm, two_ne_zero, h.symm] } } end + +end imo diff --git a/archive/imo/imo1994_q1.lean b/archive/imo/imo1994_q1.lean index bab8915e6af63..ffc8762b0e0d4 100644 --- a/archive/imo/imo1994_q1.lean +++ b/archive/imo/imo1994_q1.lean @@ -32,6 +32,8 @@ open_locale big_operators open finset +namespace imo + lemma tedious (m : ℕ) (k : fin (m+1)) : m - (m + (m + 1 - ↑k)) % (m + 1) = ↑k := begin cases k with k hk, @@ -97,3 +99,5 @@ begin -- A set of size `k+1` embed in one of size `k`, which yields a contradiction simpa [fin.coe_sub, tedious] using card_le_of_subset hf, end + +end imo diff --git a/archive/imo/imo1998_q2.lean b/archive/imo/imo1998_q2.lean index c4133b49d376e..928d78975e0d5 100644 --- a/archive/imo/imo1998_q2.lean +++ b/archive/imo/imo1998_q2.lean @@ -38,6 +38,8 @@ Rearranging gives the result. -/ open_locale classical +namespace imo + noncomputable theory /-- An ordered pair of judges. -/ @@ -212,3 +214,5 @@ begin { simp, }, { exact le_of_mul_le_mul_right h z.succ_pos, }, end + +end imo diff --git a/archive/imo/imo2001_q2.lean b/archive/imo/imo2001_q2.lean index a47afd9d539ac..bce2a35ab9b3e 100644 --- a/archive/imo/imo2001_q2.lean +++ b/archive/imo/imo2001_q2.lean @@ -30,6 +30,8 @@ open real variables {a b c : ℝ} +namespace imo + lemma denom_pos (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : 0 < a ^ 4 + b ^ 4 + c ^ 4 := add_pos (add_pos (pow_pos ha 4) (pow_pos hb 4)) (pow_pos hc 4) @@ -72,3 +74,5 @@ have h3 : ∀ {x : ℝ}, 0 < x → (x ^ (3 : ℝ)⁻¹) ^ 3 = x := λ x hx, show ↑3 = (3 : ℝ), by norm_num ▸ rpow_nat_inv_pow_nat hx.le three_ne_zero, calc 1 ≤ _ : imo2001_q2' (rpow_pos_of_pos ha _) (rpow_pos_of_pos hb _) (rpow_pos_of_pos hc _) ... = _ : by rw [h3 ha, h3 hb, h3 hc] + +end imo diff --git a/archive/imo/imo2001_q6.lean b/archive/imo/imo2001_q6.lean index c2fa9f829a855..05f09cbd59265 100644 --- a/archive/imo/imo2001_q6.lean +++ b/archive/imo/imo2001_q6.lean @@ -19,6 +19,8 @@ Prove that $a*b + c*d$ is not prime. variables {a b c d : ℤ} +namespace imo + theorem imo2001_q6 (hd : 0 < d) (hdc : d < c) (hcb : c < b) (hba : b < a) (h : a*c + b*d = (a + b - c + d) * (-a + b + c + d)) : ¬ prime (a*b + c*d) := @@ -42,3 +44,5 @@ begin have : a*c + b*d ≤ a*d + b*c, { from int.le_of_dvd aux h2 }, nlinarith only [hba, hdc, h, this] }, end + +end imo diff --git a/archive/imo/imo2005_q3.lean b/archive/imo/imo2005_q3.lean index 2c4acffbb7a11..b963c26b3ac78 100644 --- a/archive/imo/imo2005_q3.lean +++ b/archive/imo/imo2005_q3.lean @@ -18,6 +18,8 @@ factoring `(x^5-x^2)/(x^5+y^2+z^2) - (x^5-x^2)/(x^3*(x^2+y^2+z^2))` into a non-n and then making use of `xyz ≥ 1` to show `(x^5-x^2)/(x^3*(x^2+y^2+z^2)) ≥ (x^2-y*z)/(x^2+y^2+z^2)`. -/ +namespace imo + lemma key_insight (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x*y*z ≥ 1) : (x^5-x^2)/(x^5+y^2+z^2) ≥ (x^2-y*z)/(x^2+y^2+z^2) := begin @@ -59,3 +61,5 @@ begin (by linarith [sq_nonneg (x-y), sq_nonneg (y-z), sq_nonneg (z-x)]) (by linarith [sq_nonneg x, sq_nonneg y, sq_nonneg z]) }, end + +end imo diff --git a/archive/imo/imo2005_q4.lean b/archive/imo/imo2005_q4.lean index c6d854167e288..c31d8aeae822e 100644 --- a/archive/imo/imo2005_q4.lean +++ b/archive/imo/imo2005_q4.lean @@ -15,6 +15,8 @@ This is quite an easy problem, in which the key point is a modular arithmetic ca the sequence `a n` relative to an arbitrary prime. -/ +namespace imo + /-- The sequence considered in the problem, `2 ^ n + 3 ^ n + 6 ^ n - 1`. -/ def a (n : ℕ) : ℤ := 2 ^ n + 3 ^ n + 6 ^ n - 1 @@ -93,3 +95,5 @@ begin -- Contradiction! contradiction, end + +end imo diff --git a/archive/imo/imo2006_q3.lean b/archive/imo/imo2006_q3.lean index c6506dbcda082..9a266e1fb6a78 100644 --- a/archive/imo/imo2006_q3.lean +++ b/archive/imo/imo2006_q3.lean @@ -27,6 +27,8 @@ It involves making the substitution `x = a - b`, `y = b - c`, `z = c - a`, `s = a + b + c`. -/ +namespace imo + open real /-- Replacing `x` and `y` with their average increases the left side. -/ @@ -139,3 +141,5 @@ theorem imo2006_q3 (M : ℝ) : M * (a^2 + b^2 + c^2)^2) ↔ 9 * sqrt 2 / 32 ≤ M := ⟨proof₂ M, λ h _ _ _, le_trans proof₁ $ mul_le_mul_of_nonneg_right h $ sq_nonneg _⟩ + +end imo diff --git a/archive/imo/imo2006_q5.lean b/archive/imo/imo2006_q5.lean index 665882fd84f23..e170e157a1798 100644 --- a/archive/imo/imo2006_q5.lean +++ b/archive/imo/imo2006_q5.lean @@ -41,8 +41,10 @@ $P(t)+t-a-b$, and we're again done. open function polynomial +namespace imo /-- If every entry in a cyclic list of integers divides the next, then they all have the same absolute value. -/ + theorem int.nat_abs_eq_of_chain_dvd {l : cycle ℤ} {x y : ℤ} (hl : l.chain (∣)) (hx : x ∈ l) (hy : y ∈ l) : x.nat_abs = y.nat_abs := begin @@ -208,3 +210,5 @@ begin simp only [sub_eq_zero, is_root.def, eval_sub, iterate_comp_eval, eval_X] at ht, simpa [mem_roots hP', sub_eq_zero] using polynomial.is_periodic_pt_eval_two ⟨k, hk, ht⟩ end + +end imo diff --git a/archive/imo/imo2008_q2.lean b/archive/imo/imo2008_q2.lean index a20f897827eef..f633e57bbf8a9 100644 --- a/archive/imo/imo2008_q2.lean +++ b/archive/imo/imo2008_q2.lean @@ -26,6 +26,8 @@ using `c`, `m` and `n`. We factor `LHS - 1` as a square, which finishes the proo set of rational solutions to the equation, and that `W` is infinite. -/ +namespace imo + lemma subst_abc {x y z : ℝ} (h : x*y*z = 1) : ∃ a b c : ℝ, a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ x = a/b ∧ y = b/c ∧ z = c /a := begin @@ -132,3 +134,5 @@ begin exact hW_inf.mono hW_sub_S, end + +end imo diff --git a/archive/imo/imo2008_q3.lean b/archive/imo/imo2008_q3.lean index 3f8d05c99f40f..a86b5ab4fe95a 100644 --- a/archive/imo/imo2008_q3.lean +++ b/archive/imo/imo2008_q3.lean @@ -28,6 +28,8 @@ Then `p = 2n + k ≥ 2n + √(p - 4) = 2n + √(2n + k - 4) > √(2n)` and we ar open real +namespace imo + lemma p_lemma (p : ℕ) (hpp : nat.prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (hp_gt_20 : p > 20) : ∃ n : ℕ, p ∣ n ^ 2 + 1 ∧ (p : ℝ) > 2 * n + sqrt(2 * n) := begin @@ -90,3 +92,5 @@ begin exact ⟨n, hn_ge_N, p, hpp, hnat, hreal⟩, end + +end imo diff --git a/archive/imo/imo2008_q4.lean b/archive/imo/imo2008_q4.lean index b82ea5691640d..cc9889a6dec1a 100644 --- a/archive/imo/imo2008_q4.lean +++ b/archive/imo/imo2008_q4.lean @@ -23,6 +23,8 @@ The desired theorem is that either `f = λ x, x` or `f = λ x, 1/x` open real +namespace imo + lemma abs_eq_one_of_pow_eq_one (x : ℝ) (n : ℕ) (hn : n ≠ 0) (h : x ^ n = 1) : |x| = 1 := by rw [← pow_left_inj (abs_nonneg x) zero_le_one (pos_iff_ne_zero.2 hn), one_pow, pow_abs, h, abs_one] @@ -103,3 +105,5 @@ begin obtain ha₂ := abs_eq_one_of_pow_eq_one a 4 (show 4 ≠ 0, by norm_num) ha₁, rw abs_of_pos ha at ha₂, rw ha₂ at hfa₁, norm_num at hfa₁ }, end + +end imo diff --git a/archive/imo/imo2011_q3.lean b/archive/imo/imo2011_q3.lean index c3e5dfc5d8361..1889e503ef54b 100644 --- a/archive/imo/imo2011_q3.lean +++ b/archive/imo/imo2011_q3.lean @@ -20,6 +20,8 @@ for all x and y. Prove that f(x) = 0 for all x ≤ 0. Direct translation of the solution found in https://www.imo-official.org/problems/IMO2011SL.pdf -/ +namespace imo + theorem imo2011_q3 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) ≤ y * f x + f (f x)) : ∀ x ≤ 0, f x = 0 := begin @@ -68,3 +70,5 @@ begin rw hno at hp, linarith }, end + +end imo diff --git a/archive/imo/imo2011_q5.lean b/archive/imo/imo2011_q5.lean index abf6897ad352d..5fe984f6114a6 100644 --- a/archive/imo/imo2011_q5.lean +++ b/archive/imo/imo2011_q5.lean @@ -17,6 +17,8 @@ of positive integers. Suppose that, for any two integers open int +namespace imo + theorem imo2011_q5 (f : ℤ → ℤ) (hpos : ∀ n : ℤ, 0 < f n) (hdvd : ∀ m n : ℤ, f (m - n) ∣ f m - f n) : ∀ m n : ℤ, f m ≤ f n → f m ∣ f n := @@ -57,3 +59,5 @@ begin { -- m = n rw h_fm_eq_fn } end + +end imo diff --git a/archive/imo/imo2013_q1.lean b/archive/imo/imo2013_q1.lean index 0b6b4680cc777..a2b0315d2f37e 100644 --- a/archive/imo/imo2013_q1.lean +++ b/archive/imo/imo2013_q1.lean @@ -27,6 +27,8 @@ We prove a slightly more general version where k does not need to be strictly po open_locale big_operators +namespace imo + lemma arith_lemma (k n : ℕ) : 0 < 2 * n + 2^k.succ := calc 0 < 2 : zero_lt_two ... = 2^1 : (pow_one 2).symm @@ -101,3 +103,5 @@ begin (1 + 1 / ↑(m pk)) : by rw [prod_lemma, hpm, ←hmpk, mul_comm] ... = ∏ i in finset.range pk.succ, (1 + 1 / m i) : by rw ← finset.prod_range_succ _ pk } end + +end imo diff --git a/archive/imo/imo2013_q5.lean b/archive/imo/imo2013_q5.lean index 53cb83b0df515..d27aa509953e8 100644 --- a/archive/imo/imo2013_q5.lean +++ b/archive/imo/imo2013_q5.lean @@ -29,6 +29,8 @@ https://www.imo-official.org/problems/IMO2013SL.pdf open_locale big_operators +namespace imo + lemma le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y) (h : ∀ n : ℕ, 0 < n → x^n - 1 < y^n) : x ≤ y := @@ -301,3 +303,5 @@ begin ... = (((x2num : ℚ) / (x2denom : ℚ) : ℚ) : ℝ) : by norm_cast ... = x : by rw ←hrat_expand2 end + +end imo diff --git a/archive/imo/imo2019_q1.lean b/archive/imo/imo2019_q1.lean index b19fd9475f693..46d3bffacab40 100644 --- a/archive/imo/imo2019_q1.lean +++ b/archive/imo/imo2019_q1.lean @@ -19,6 +19,8 @@ Note that there is a much more compact proof of this fact in Isabelle/HOL - http://downthetypehole.de/paste/4YbGgqb4 -/ +namespace imo + theorem imo2019Q1 (f : ℤ → ℤ) : (∀ a b : ℤ, f (2 * a) + 2 * (f b) = f (f (a + b))) ↔ (f = 0) ∨ ∃ c, f = λ x, 2 * x + c := @@ -49,3 +51,5 @@ begin { right, use c, ext b, simp [H, add_comm] }, { left, ext b, simpa [H, two_ne_zero] using H3 } end + +end imo diff --git a/archive/imo/imo2019_q2.lean b/archive/imo/imo2019_q2.lean index ca6781c82a7e5..35d005480df5f 100644 --- a/archive/imo/imo2019_q2.lean +++ b/archive/imo/imo2019_q2.lean @@ -56,6 +56,8 @@ rather than more literally with `affine_segment`. -/ library_note "IMO geometry formalization conventions" +namespace imo + noncomputable theory open affine affine.simplex euclidean_geometry finite_dimensional @@ -591,3 +593,5 @@ theorem imo2019_q2 (A B C A₁ B₁ P Q P₁ Q₁ : Pt) (⟨A, B, C, A₁, B₁, P, Q, P₁, Q₁, affine_independent_ABC, wbtw_B_A₁_C, wbtw_A_B₁_C, wbtw_A_P_A₁, wbtw_B_Q_B₁, PQ_parallel_AB, P_ne_Q, sbtw_P_B₁_P₁, angle_PP₁C_eq_angle_BAC, C_ne_P₁, sbtw_Q_A₁_Q₁, angle_CQ₁Q_eq_angle_CBA, C_ne_Q₁⟩ : imo2019q2_cfg V Pt).result + +end imo diff --git a/archive/imo/imo2019_q4.lean b/archive/imo/imo2019_q4.lean index a4d25853dab7f..dfc00ea7b44d8 100644 --- a/archive/imo/imo2019_q4.lean +++ b/archive/imo/imo2019_q4.lean @@ -26,6 +26,8 @@ individually. open_locale nat big_operators open finset multiplicity nat (hiding zero_le prime) +namespace imo + theorem imo2019_q4_upper_bound {k n : ℕ} (hk : k > 0) (h : (k! : ℤ) = ∏ i in range n, (2 ^ n - 2 ^ i)) : n < 6 := begin @@ -92,3 +94,5 @@ begin /- n = 5 -/ { refine monotone_factorial.ne_of_lt_of_lt_nat 10 _ _ _ h; norm_num }, end + +end imo diff --git a/archive/imo/imo2020_q2.lean b/archive/imo/imo2020_q2.lean index beea58a78ff17..4bc2f471ae33d 100644 --- a/archive/imo/imo2020_q2.lean +++ b/archive/imo/imo2020_q2.lean @@ -21,6 +21,8 @@ the official solutions. open real +namespace imo + theorem imo2020_q2 (a b c d : ℝ) (hd0 : 0 < d) (hdc : d ≤ c) (hcb : c ≤ b) (hba : b ≤ a) (h1 : a + b + c + d = 1) : (a + 2 * b + 3 * c + 4 * d) * a ^ a * b ^ b * c ^ c * d ^ d < 1 := @@ -44,3 +46,5 @@ begin ... = (a + b + c + d) ^ 3 : by ring ... = 1 : by simp [h1] end + +end imo diff --git a/archive/imo/imo2021_q1.lean b/archive/imo/imo2021_q1.lean index 4a123aeaa0f51..4a8f457c42722 100644 --- a/archive/imo/imo2021_q1.lean +++ b/archive/imo/imo2021_q1.lean @@ -43,6 +43,8 @@ which finishes the proof. open real +namespace imo + lemma lower_bound (n l : ℕ) (hl : 2 + sqrt (4 + 2 * n) ≤ 2 * l) : n + 4 * l ≤ 2 * l * l := begin @@ -178,3 +180,5 @@ begin cases hCA; [right, left]; exact ⟨a, (hCA ha).2, b, (hCA hb).2, hab, h₁ a (hCA ha).1 b (hCA hb).1 hab⟩, end + +end imo diff --git a/archive/oxford_invariants/2021summer/week3_p1.lean b/archive/oxford_invariants/2021summer/week3_p1.lean index d0a8fb0731ff8..eb30161c3a81c 100644 --- a/archive/oxford_invariants/2021summer/week3_p1.lean +++ b/archive/oxford_invariants/2021summer/week3_p1.lean @@ -72,7 +72,7 @@ open_locale big_operators variables {α : Type*} [linear_ordered_field α] -theorem week3_p1 (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤ n, 0 < a i) +theorem oxford_invariants.week3_p1 (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤ n, 0 < a i) (ha : ∀ i, i + 2 ≤ n → a (i + 1) ∣ a i + a (i + 2)) : ∃ b : ℕ, (b : α) = ∑ i in finset.range n, (a 0 * a n)/(a i * a (i + 1)) := begin diff --git a/archive/sensitivity.lean b/archive/sensitivity.lean index c2c46c393fd79..995ff612ae9c3 100644 --- a/archive/sensitivity.lean +++ b/archive/sensitivity.lean @@ -33,6 +33,8 @@ The project was developed at https://github.com/leanprover-community/lean-sensit archived at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean -/ +namespace sensitivity + /-! The next two lines assert we do not want to give a constructive proof, but rather use classical logic. -/ noncomputable theory @@ -435,3 +437,5 @@ begin convert finset.inter_subset_inter_right coeffs_support end end + +end sensitivity diff --git a/counterexamples/canonically_ordered_comm_semiring_two_mul.lean b/counterexamples/canonically_ordered_comm_semiring_two_mul.lean index fd6ca5897584d..012d49af2dcee 100644 --- a/counterexamples/canonically_ordered_comm_semiring_two_mul.lean +++ b/counterexamples/canonically_ordered_comm_semiring_two_mul.lean @@ -23,6 +23,8 @@ Reference: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology -/ +namespace counterexample + namespace from_Bhavik /-- Bhavik Mehta's example. There are only the initial definitions, but no proofs. The Type @@ -265,3 +267,5 @@ begin end end ex_L + +end counterexample diff --git a/counterexamples/char_p_zero_ne_char_zero.lean b/counterexamples/char_p_zero_ne_char_zero.lean index 36fd17d6adcf9..a6b9cecde95cc 100644 --- a/counterexamples/char_p_zero_ne_char_zero.lean +++ b/counterexamples/char_p_zero_ne_char_zero.lean @@ -18,6 +18,8 @@ This file shows that there are semiring `R` for which `char_p R 0` holds and `ch The example is `{0, 1}` with saturating addition. -/ +namespace counterexample + @[simp] lemma add_one_eq_one (x : with_zero unit) : x + 1 = 1 := with_zero.cases_on x (by refl) (λ h, by refl) @@ -26,3 +28,5 @@ lemma with_zero_unit_char_p_zero : char_p (with_zero unit) 0 := lemma with_zero_unit_not_char_zero : ¬ char_zero (with_zero unit) := λ ⟨h⟩, h.ne (by simp : 1 + 1 ≠ 0 + 1) (by simp) + +end counterexample diff --git a/counterexamples/cyclotomic_105.lean b/counterexamples/cyclotomic_105.lean index d600a7098a3d5..cfbb5aa23bb94 100644 --- a/counterexamples/cyclotomic_105.lean +++ b/counterexamples/cyclotomic_105.lean @@ -16,6 +16,8 @@ theorem `not_forall_coeff_cyclotomic_neg_one_zero_one`. We prove this with the c open nat (proper_divisors) finset +namespace counterexample + section computation instance nat.fact_prime_five : fact (nat.prime 5) := ⟨by norm_num⟩ @@ -100,3 +102,5 @@ begin rw coeff_cyclotomic_105 at h, norm_num at h end + +end counterexample diff --git a/counterexamples/direct_sum_is_internal.lean b/counterexamples/direct_sum_is_internal.lean index c9febdae9b63d..9a4b75ece1807 100644 --- a/counterexamples/direct_sum_is_internal.lean +++ b/counterexamples/direct_sum_is_internal.lean @@ -19,6 +19,8 @@ This file demonstrates why `direct_sum.is_internal_submodule_of_independent_of_s take `ring R` and not `semiring R`. -/ +namespace counterexample + lemma units_int.one_ne_neg_one : (1 : ℤˣ) ≠ -1 := dec_trivial /-- Submodules of positive and negative integers, keyed by sign. -/ @@ -93,3 +95,5 @@ end /-- And so they do not represent an internal direct sum. -/ lemma with_sign.not_internal : ¬direct_sum.is_internal with_sign := with_sign.not_injective ∘ and.elim_left + +end counterexample diff --git a/counterexamples/girard.lean b/counterexamples/girard.lean index 218c892caa71e..090551161b38a 100644 --- a/counterexamples/girard.lean +++ b/counterexamples/girard.lean @@ -24,6 +24,8 @@ Based on Watkins' LF implementation of Hurkens' simplification of Girard's parad * `girard`: there are no Girard universes. -/ +namespace counterexample + /-- **Girard's paradox**: there are no universes `u` such that `Type u : Type u`. Since we can't actually change the type of Lean's `Π` operator, we assume the existence of `pi`, `lam`, `app` and the `beta` rule equivalent to the `Π` and `app` constructors of type theory. @@ -43,3 +45,5 @@ let ω : set (set U) := {p | ∀ x, p ∈ σ x → x ∈ p} in let δ (S : set (set U)) := ∀ p, p ∈ S → τ S ∈ p in have δ ω := λ p d, d (τ ω) $ στ.2 $ λ x h, d (τ (σ x)) (στ.2 h), this {y | ¬ δ (σ y)} (λ x e f, f _ e (λ p h, f _ (στ.1 h))) (λ p h, this _ (στ.1 h)) + +end counterexample diff --git a/counterexamples/homogeneous_prime_not_prime.lean b/counterexamples/homogeneous_prime_not_prime.lean index 8692774542313..1e895db644e53 100644 --- a/counterexamples/homogeneous_prime_not_prime.lean +++ b/counterexamples/homogeneous_prime_not_prime.lean @@ -30,6 +30,8 @@ prime. But it is homogeneously prime, i.e. if `(a, b), (c, d)` are two homogeneo homogeneous, prime -/ +namespace counterexample + namespace counterexample_not_prime_but_homogeneous_prime open direct_sum @@ -152,3 +154,5 @@ begin end end counterexample_not_prime_but_homogeneous_prime + +end counterexample diff --git a/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean b/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean index 6e08c5f9f847f..0fac502d4e5e3 100644 --- a/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean +++ b/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean @@ -18,6 +18,8 @@ Relevant Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/mul_pos -/ +namespace counterexample + /-- The three element monoid. -/ @[derive [decidable_eq]] inductive foo @@ -85,3 +87,5 @@ end example : 0 < ε ∧ ε * ε = 0 := by boom end foo + +end counterexample diff --git a/counterexamples/map_floor.lean b/counterexamples/map_floor.lean index b1c262d6d780c..2fd1b31c7cedc 100644 --- a/counterexamples/map_floor.lean +++ b/counterexamples/map_floor.lean @@ -33,6 +33,8 @@ But it does not preserve floors (nor ceils) as `⌊-ε⌋ = -1` while `⌊f (-ε (`int_with_epsilons.forget_epsilons_floor_lt`, `int_with_epsilons.lt_forget_epsilons_ceil`). -/ +namespace counterexample + noncomputable theory open function int polynomial @@ -124,3 +126,5 @@ begin end end int_with_epsilon + +end counterexample diff --git a/counterexamples/phillips.lean b/counterexamples/phillips.lean index 82bdaa79e5d5d..eafafd6d169bd 100644 --- a/counterexamples/phillips.lean +++ b/counterexamples/phillips.lean @@ -72,6 +72,8 @@ on a discrete copy of the original type, as mathlib only contains the space of a continuous functions (which is the useful one). -/ +namespace counterexample + universe u variables {α : Type u} open set bounded_continuous_function measure_theory @@ -606,3 +608,5 @@ begin end end phillips_1940 + +end counterexample diff --git a/counterexamples/pseudoelement.lean b/counterexamples/pseudoelement.lean index 5a28cf838eabb..0e2ddaf8cc23b 100644 --- a/counterexamples/pseudoelement.lean +++ b/counterexamples/pseudoelement.lean @@ -31,9 +31,11 @@ given by `t ↦ (t, 2 * t)` and `y : ℚ ⟶ ℚ ⊞ ℚ` given by `t ↦ (t, t) open category_theory.abelian category_theory category_theory.limits Module linear_map +namespace counterexample + noncomputable theory -namespace category_theory.abelian.pseudoelement +open category_theory.abelian.pseudoelement /-- `x` is given by `t ↦ (t, 2 * t)`. -/ def x : over ((of ℤ ℚ) ⊞ (of ℤ ℚ)) := @@ -119,4 +121,4 @@ lemma exist_ne_and_fst_eq_fst_and_snd_eq_snd : ∃ x y : (of ℤ ℚ) ⊞ (of (biprod.snd : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) x = (biprod.snd : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) y:= ⟨⟦x⟧, ⟦y⟧, mk_x_ne_mk_y, fst_mk_x_eq_fst_mk_y, snd_mk_x_eq_snd_mk_y⟩ -end category_theory.abelian.pseudoelement +end counterexample diff --git a/counterexamples/quadratic_form.lean b/counterexamples/quadratic_form.lean index 20af196c19f52..d9f029822dce1 100644 --- a/counterexamples/quadratic_form.lean +++ b/counterexamples/quadratic_form.lean @@ -19,6 +19,8 @@ variables (F : Type*) [nontrivial F] [comm_ring F] [char_p F 2] open bilin_form +namespace counterexample + /-- The bilinear form we will use as a counterexample, over some field `F` of characteristic two. -/ def B : bilin_form F (F × F) := bilin_form.lin_mul_lin (linear_map.fst _ _ _) (linear_map.snd _ _ _) @@ -51,3 +53,5 @@ begin rw [bilin_form.to_quadratic_form_zero, bilin_form.to_quadratic_form_eq_zero], exact is_alt_B F, end + +end counterexample diff --git a/counterexamples/seminorm_lattice_not_distrib.lean b/counterexamples/seminorm_lattice_not_distrib.lean index 7963e3e7a07ef..95b4e997ea397 100644 --- a/counterexamples/seminorm_lattice_not_distrib.lean +++ b/counterexamples/seminorm_lattice_not_distrib.lean @@ -20,6 +20,8 @@ This proves the lattice `seminorm ℝ (ℝ × ℝ)` is not distributive. open seminorm open_locale nnreal +namespace counterexample + namespace seminorm_not_distrib @[simps] noncomputable def p : seminorm ℝ (ℝ×ℝ) := @@ -68,3 +70,5 @@ begin end end seminorm_not_distrib + +end counterexample diff --git a/counterexamples/sorgenfrey_line.lean b/counterexamples/sorgenfrey_line.lean index f96879bbd74c9..065ecbecd57b5 100644 --- a/counterexamples/sorgenfrey_line.lean +++ b/counterexamples/sorgenfrey_line.lean @@ -32,6 +32,8 @@ Prove that the Sorgenfrey line is a paracompact space. open set filter topological_space open_locale topology filter +namespace counterexample + noncomputable theory /-- The Sorgenfrey line. It is the real line with the topology space structure generated by @@ -294,3 +296,5 @@ lemma not_second_countable_topology : ¬second_countable_topology ℝₗ := by { introI, exact not_metrizable_space (metrizable_space_of_t3_second_countable _) } end sorgenfrey_line + +end counterexample diff --git a/counterexamples/zero_divisors_in_add_monoid_algebras.lean b/counterexamples/zero_divisors_in_add_monoid_algebras.lean index da188dfa571cb..88e430e411b30 100644 --- a/counterexamples/zero_divisors_in_add_monoid_algebras.lean +++ b/counterexamples/zero_divisors_in_add_monoid_algebras.lean @@ -41,6 +41,8 @@ finitely supported function is lexicographic, matching the list notation. The i -/ open finsupp add_monoid_algebra +namespace counterexample + /-- This is a simple example showing that if `R` is a non-trivial ring and `A` is an additive monoid with an element `a` satisfying `n • a = a` and `(n - 1) • a ≠ a`, for some `2 ≤ n`, then `add_monoid_algebra R A` contains non-zero zero-divisors. The elements are easy to write down: @@ -230,3 +232,5 @@ begin { simpa [unique_add] }, exact λ x y, ⟨x - 1, y + 1, sub_add_add_cancel _ _ _, by simp⟩, end + +end counterexample