From cff52ba43246cabdc2a877421f98269f8fa57795 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed, 15 Nov 2023 20:16:30 +0000 Subject: [PATCH] chore: tidy various files (#8409) --- .../Algebra/CovariantAndContravariant.lean | 2 +- Mathlib/Algebra/Group/UniqueProds.lean | 14 +-- .../Algebra/MonoidAlgebra/NoZeroDivisors.lean | 4 +- Mathlib/Analysis/Convex/Cone/Proper.lean | 32 +++--- Mathlib/Data/Polynomial/Div.lean | 2 +- Mathlib/Data/Polynomial/Inductions.lean | 8 +- .../MeasureTheory/Measure/VectorMeasure.lean | 6 +- Mathlib/ModelTheory/Algebra/Field/Basic.lean | 10 +- Mathlib/Order/Filter/Basic.lean | 4 +- Mathlib/Order/Monotone/Basic.lean | 24 ++--- Mathlib/Topology/AlexandrovDiscrete.lean | 97 ++++++++++--------- 11 files changed, 102 insertions(+), 101 deletions(-) diff --git a/Mathlib/Algebra/CovariantAndContravariant.lean b/Mathlib/Algebra/CovariantAndContravariant.lean index fbf97fb28d99eb..e6e66200dcee3b 100644 --- a/Mathlib/Algebra/CovariantAndContravariant.lean +++ b/Mathlib/Algebra/CovariantAndContravariant.lean @@ -43,7 +43,7 @@ A formal remark is that normally `CovariantClass` uses the `(≤)`-relation, whi `ContravariantClass` uses the `(<)`-relation. This need not be the case in general, but seems to be the most common usage. In the opposite direction, the implication ```lean -[Semigroup α] [PartialOrder α] [ContravariantClass α α (*) (≤)] ↦ LeftCancelSemigroup α +[Semigroup α] [PartialOrder α] [ContravariantClass α α (*) (≤)] → LeftCancelSemigroup α ``` holds -- note the `Co*ntra*` assumption on the `(≤)`-relation. diff --git a/Mathlib/Algebra/Group/UniqueProds.lean b/Mathlib/Algebra/Group/UniqueProds.lean index b61e40e3d75b67..92709b69811edb 100644 --- a/Mathlib/Algebra/Group/UniqueProds.lean +++ b/Mathlib/Algebra/Group/UniqueProds.lean @@ -203,7 +203,7 @@ theorem to_mulOpposite (h : UniqueMul A B a0 b0) : theorem iff_mulOpposite : UniqueMul (B.map ⟨_, op_injective⟩) (A.map ⟨_, op_injective⟩) (op b0) (op a0) ↔ UniqueMul A B a0 b0 := -⟨of_mulOpposite, to_mulOpposite⟩ + ⟨of_mulOpposite, to_mulOpposite⟩ end Opposites @@ -332,7 +332,7 @@ theorem mulHom_image_of_injective (f : H →ₙ* G) (hf : Function.Injective f) @[to_additive "`UniqueSums` is preserved under additive equivalences."] theorem mulHom_image_iff (f : G ≃* H) : UniqueProds G ↔ UniqueProds H := -⟨mulHom_image_of_injective f.symm f.symm.injective, mulHom_image_of_injective f f.injective⟩ + ⟨mulHom_image_of_injective f.symm f.symm.injective, mulHom_image_of_injective f f.injective⟩ open Finset MulOpposite in @[to_additive] @@ -500,7 +500,7 @@ theorem mulHom_image_of_injective (f : H →ₙ* G) (hf : Function.Injective f) /-- `TwoUniqueProd` is preserved under multiplicative equivalences. -/ @[to_additive "`TwoUniqueSums` is preserved under additive equivalences."] theorem mulHom_image_iff (f : G ≃* H) : TwoUniqueProds G ↔ TwoUniqueProds H := -⟨mulHom_image_of_injective f.symm f.symm.injective, mulHom_image_of_injective f f.injective⟩ + ⟨mulHom_image_of_injective f.symm f.symm.injective, mulHom_image_of_injective f f.injective⟩ @[to_additive] instance {ι} (G : ι → Type*) [∀ i, Mul (G i)] [∀ i, TwoUniqueProds (G i)] : TwoUniqueProds (∀ i, G i) where @@ -564,7 +564,7 @@ theorem of_mulOpposite (h : TwoUniqueProds Gᵐᵒᵖ) : TwoUniqueProds G where @[to_additive "This instance asserts that if `G` has a right-cancellative addition, a linear order, and addition is strictly monotone w.r.t. the second argument, then `G` has `TwoUniqueSums`." ] -instance (priority := 100) of_Covariant_right [IsRightCancelMul G] +instance (priority := 100) of_covariant_right [IsRightCancelMul G] [LinearOrder G] [CovariantClass G G (· * ·) (· < ·)] : TwoUniqueProds G where uniqueMul_of_one_lt_card {A B} hc := by @@ -598,13 +598,13 @@ open MulOpposite in @[to_additive "This instance asserts that if `G` has a left-cancellative addition, a linear order, and addition is strictly monotone w.r.t. the first argument, then `G` has `TwoUniqueSums`." ] -instance (priority := 100) of_Covariant_left [IsLeftCancelMul G] +instance (priority := 100) of_covariant_left [IsLeftCancelMul G] [LinearOrder G] [CovariantClass G G (Function.swap (· * ·)) (· < ·)] : TwoUniqueProds G := let _ := LinearOrder.lift' (unop : Gᵐᵒᵖ → G) unop_injective let _ : CovariantClass Gᵐᵒᵖ Gᵐᵒᵖ (· * ·) (· < ·) := - { elim := fun _ _ _ bc ↦ mul_lt_mul_right' (α := G) bc (unop _) } - of_mulOpposite of_Covariant_right + { elim := fun _ _ _ bc ↦ mul_lt_mul_right' (α := G) bc (unop _) } + of_mulOpposite of_covariant_right end TwoUniqueProds diff --git a/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean b/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean index b93c62385962db..226b04d52247fb 100644 --- a/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean +++ b/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean @@ -97,9 +97,9 @@ as a product of monomials in the supports of `f` and `g` is a product. -/ theorem mul_apply_add_eq_mul_of_uniqueAdd [Add A] {f g : R[A]} {a0 b0 : A} (h : UniqueAdd f.support g.support a0 b0) : (f * g) (a0 + b0) = f a0 * g b0 := -MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul (A := Multiplicative A) h + MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul (A := Multiplicative A) h instance [NoZeroDivisors R] [Add A] [UniqueSums A] : NoZeroDivisors R[A] := -MonoidAlgebra.instNoZeroDivisorsOfUniqueProds (A := Multiplicative A) + MonoidAlgebra.instNoZeroDivisorsOfUniqueProds (A := Multiplicative A) end AddMonoidAlgebra diff --git a/Mathlib/Analysis/Convex/Cone/Proper.lean b/Mathlib/Analysis/Convex/Cone/Proper.lean index 9cefd9b847b658..f870e73b293d30 100644 --- a/Mathlib/Analysis/Convex/Cone/Proper.lean +++ b/Mathlib/Analysis/Convex/Cone/Proper.lean @@ -75,7 +75,7 @@ cone programs and proving duality theorems. -/ structure ProperCone (𝕜 : Type*) (E : Type*) [OrderedSemiring 𝕜] [AddCommMonoid E] [TopologicalSpace E] [SMul 𝕜 E] extends ConvexCone 𝕜 E where nonempty' : (carrier : Set E).Nonempty - is_closed' : IsClosed (carrier : Set E) + isClosed' : IsClosed (carrier : Set E) #align proper_cone ProperCone namespace ProperCone @@ -86,14 +86,16 @@ variable {𝕜 : Type*} [OrderedSemiring 𝕜] variable {E : Type*} [AddCommMonoid E] [TopologicalSpace E] [SMul 𝕜 E] +attribute [coe] toConvexCone + instance : Coe (ProperCone 𝕜 E) (ConvexCone 𝕜 E) := - ⟨fun K => K.1⟩ + ⟨toConvexCone⟩ -- Porting note: now a syntactic tautology -- @[simp] -- theorem toConvexCone_eq_coe (K : ProperCone 𝕜 E) : K.toConvexCone = K := -- rfl --- #align proper_cone.to_convex_cone_eq_coe ProperCone.toConvexCone_eq_coe +#noalign proper_cone.to_convex_cone_eq_coe theorem ext' : Function.Injective ((↑) : ProperCone 𝕜 E → ConvexCone 𝕜 E) := fun S T h => by cases S; cases T; congr @@ -119,7 +121,7 @@ protected theorem nonempty (K : ProperCone 𝕜 E) : (K : Set E).Nonempty := #align proper_cone.nonempty ProperCone.nonempty protected theorem isClosed (K : ProperCone 𝕜 E) : IsClosed (K : Set E) := - K.is_closed' + K.isClosed' #align proper_cone.is_closed ProperCone.isClosed end SMul @@ -135,7 +137,7 @@ module. -/ def positive : ProperCone 𝕜 E where toConvexCone := ConvexCone.positive 𝕜 E nonempty' := ⟨0, ConvexCone.pointed_positive _ _⟩ - is_closed' := isClosed_Ici + isClosed' := isClosed_Ici @[simp] theorem mem_positive {x : E} : x ∈ positive 𝕜 E ↔ 0 ≤ x := @@ -156,7 +158,7 @@ variable {E : Type*} [AddCommMonoid E] [TopologicalSpace E] [T1Space E] [Module instance : Zero (ProperCone 𝕜 E) := ⟨{ toConvexCone := 0 nonempty' := ⟨0, rfl⟩ - is_closed' := isClosed_singleton }⟩ + isClosed' := isClosed_singleton }⟩ instance : Inhabited (ProperCone 𝕜 E) := ⟨0⟩ @@ -166,7 +168,7 @@ theorem mem_zero (x : E) : x ∈ (0 : ProperCone 𝕜 E) ↔ x = 0 := Iff.rfl #align proper_cone.mem_zero ProperCone.mem_zero -@[simp] -- Porting note: removed `norm_cast` (new-style structures) +@[simp, norm_cast] theorem coe_zero : ↑(0 : ProperCone 𝕜 E) = (0 : ConvexCone 𝕜 E) := rfl #align proper_cone.coe_zero ProperCone.coe_zero @@ -194,10 +196,10 @@ noncomputable def map (f : E →L[ℝ] F) (K : ProperCone ℝ E) : ProperCone toConvexCone := ConvexCone.closure (ConvexCone.map (f : E →ₗ[ℝ] F) ↑K) nonempty' := ⟨0, subset_closure <| SetLike.mem_coe.2 <| ConvexCone.mem_map.2 ⟨0, K.pointed, map_zero _⟩⟩ - is_closed' := isClosed_closure + isClosed' := isClosed_closure #align proper_cone.map ProperCone.map -@[simp] -- Porting note: removed `norm_cast` (new-style structures) +@[simp, norm_cast] theorem coe_map (f : E →L[ℝ] F) (K : ProperCone ℝ E) : ↑(K.map f) = (ConvexCone.map (f : E →ₗ[ℝ] F) ↑K).closure := rfl @@ -218,10 +220,10 @@ theorem map_id (K : ProperCone ℝ E) : K.map (ContinuousLinearMap.id ℝ E) = K def dual (K : ProperCone ℝ E) : ProperCone ℝ E where toConvexCone := (K : Set E).innerDualCone nonempty' := ⟨0, pointed_innerDualCone _⟩ - is_closed' := isClosed_innerDualCone _ + isClosed' := isClosed_innerDualCone _ #align proper_cone.dual ProperCone.dual -@[simp] -- Porting note: removed `norm_cast` (new-style structures) +@[simp, norm_cast] theorem coe_dual (K : ProperCone ℝ E) : ↑(dual K) = (K : Set E).innerDualCone := rfl #align proper_cone.coe_dual ProperCone.coe_dual @@ -232,14 +234,13 @@ theorem mem_dual {K : ProperCone ℝ E} {y : E} : y ∈ dual K ↔ ∀ ⦃x⦄, #align proper_cone.mem_dual ProperCone.mem_dual /-- The preimage of a proper cone under a continuous `ℝ`-linear map is a proper cone. -/ -noncomputable def comap (f : E →L[ℝ] F) (S : ProperCone ℝ F) : ProperCone ℝ E - where +noncomputable def comap (f : E →L[ℝ] F) (S : ProperCone ℝ F) : ProperCone ℝ E where toConvexCone := ConvexCone.comap (f : E →ₗ[ℝ] F) S nonempty' := ⟨0, by simp only [ConvexCone.comap, mem_preimage, map_zero, SetLike.mem_coe, mem_coe] apply ProperCone.pointed⟩ - is_closed' := by + isClosed' := by simp only [ConvexCone.comap, ContinuousLinearMap.coe_coe] apply IsClosed.preimage f.2 S.isClosed #align proper_cone.comap ProperCone.comap @@ -292,8 +293,7 @@ theorem hyperplane_separation (K : ProperCone ℝ E) {f : E →L[ℝ] F} {b : F} ConvexCone.mem_closure, mem_closure_iff_seq_limit] -- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b` rintro ⟨seq, hmem, htends⟩ y hinner - suffices h : ∀ n, 0 ≤ ⟪y, seq n⟫_ℝ; - exact + suffices h : ∀ n, 0 ≤ ⟪y, seq n⟫_ℝ from ge_of_tendsto' (Continuous.seqContinuous (Continuous.inner (@continuous_const _ _ _ _ y) continuous_id) htends) diff --git a/Mathlib/Data/Polynomial/Div.lean b/Mathlib/Data/Polynomial/Div.lean index ecf463b19f262c..fbc3e930be0c5e 100644 --- a/Mathlib/Data/Polynomial/Div.lean +++ b/Mathlib/Data/Polynomial/Div.lean @@ -237,7 +237,7 @@ theorem degree_modByMonic_le (p : R[X]) {q : R[X]} (hq : Monic q) : degree (p % theorem natDegree_modByMonic_le (p : Polynomial R) {g : Polynomial R} (hg : g.Monic) : natDegree (p %ₘ g) ≤ g.natDegree := -natDegree_le_natDegree (degree_modByMonic_le p hg) + natDegree_le_natDegree (degree_modByMonic_le p hg) end Ring diff --git a/Mathlib/Data/Polynomial/Inductions.lean b/Mathlib/Data/Polynomial/Inductions.lean index 5b4f3de4e81179..ef91eb3f944ee0 100644 --- a/Mathlib/Data/Polynomial/Inductions.lean +++ b/Mathlib/Data/Polynomial/Inductions.lean @@ -94,9 +94,9 @@ theorem divX_X_pow : divX (X ^ n : R[X]) = if (n = 0) then 0 else X ^ (n - 1) := /-- `divX` as an additive homomorphism. -/ noncomputable def divX_hom : R[X] →+ R[X] := -{ toFun := divX - map_zero' := divX_zero - map_add' := fun _ _ => divX_add } + { toFun := divX + map_zero' := divX_zero + map_add' := fun _ _ => divX_add } @[simp] theorem divX_hom_toFun : divX_hom p = divX p := rfl @@ -111,7 +111,7 @@ theorem natDegree_divX_eq_natDegree_tsub_one : p.divX.natDegree = p.natDegree - · exact natDegree_C_mul_X_pow (n - 1) c c0 theorem natDegree_divX_le : p.divX.natDegree ≤ p.natDegree := -natDegree_divX_eq_natDegree_tsub_one.trans_le (Nat.pred_le _) + natDegree_divX_eq_natDegree_tsub_one.trans_le (Nat.pred_le _) theorem divX_C_mul_X_pow : divX (C a * X ^ n) = if n = 0 then 0 else C a * X ^ (n - 1) := by simp only [divX_C_mul, divX_X_pow, mul_ite, mul_zero] diff --git a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean index 364c958f26b701..69aedbea53977b 100644 --- a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean @@ -54,7 +54,7 @@ variable {α β : Type*} {m : MeasurableSpace α} /-- A vector measure on a measurable space `α` is a σ-additive `M`-valued function (for some `M` an add monoid) such that the empty set and non-measurable sets are mapped to zero. -/ structure VectorMeasure (α : Type*) [MeasurableSpace α] (M : Type*) [AddCommMonoid M] - [TopologicalSpace M] where + [TopologicalSpace M] where measureOf' : Set α → M empty' : measureOf' ∅ = 0 not_measurable' ⦃i : Set α⦄ : ¬MeasurableSet i → measureOf' i = 0 @@ -701,8 +701,7 @@ theorem restrict_univ : v.restrict Set.univ = v := theorem restrict_zero {i : Set α} : (0 : VectorMeasure α M).restrict i = 0 := by by_cases hi : MeasurableSet i · ext j hj - rw [restrict_apply 0 hi hj] - rfl + rw [restrict_apply 0 hi hj, zero_apply, zero_apply] · exact dif_neg hi #align measure_theory.vector_measure.restrict_zero MeasureTheory.VectorMeasure.restrict_zero @@ -1151,7 +1150,6 @@ def MutuallySingular (v : VectorMeasure α M) (w : VectorMeasure α N) : Prop := ∃ s : Set α, MeasurableSet s ∧ (∀ (t) (_ : t ⊆ s), v t = 0) ∧ ∀ (t) (_ : t ⊆ sᶜ), w t = 0 #align measure_theory.vector_measure.mutually_singular MeasureTheory.VectorMeasure.MutuallySingular --- mathport name: vector_measure.mutually_singular @[inherit_doc VectorMeasure.MutuallySingular] scoped[MeasureTheory] infixl:60 " ⟂ᵥ " => MeasureTheory.VectorMeasure.MutuallySingular diff --git a/Mathlib/ModelTheory/Algebra/Field/Basic.lean b/Mathlib/ModelTheory/Algebra/Field/Basic.lean index acbdd7b70d9d67..9d256204f23ef3 100644 --- a/Mathlib/ModelTheory/Algebra/Field/Basic.lean +++ b/Mathlib/ModelTheory/Algebra/Field/Basic.lean @@ -45,7 +45,7 @@ inductive FieldAxiom : Type | oneMul : FieldAxiom | existsInv : FieldAxiom | leftDistrib : FieldAxiom - | existsPairNe : FieldAxiom + | existsPairNE : FieldAxiom /-- The first order sentence corresponding to each field axiom -/ @[simp] @@ -58,7 +58,7 @@ def FieldAxiom.toSentence : FieldAxiom → Language.ring.Sentence | .oneMul => ∀' (((1 : Language.ring.Term _) * &0) =' &0) | .existsInv => ∀' (∼(&0 =' 0) ⟹ ∃' ((&0 * &1) =' 1)) | .leftDistrib => ∀' ∀' ∀' ((&0 * (&1 + &2)) =' ((&0 * &1) + (&0 * &2))) - | .existsPairNe => ∃' ∃' (∼(&0 =' &1)) + | .existsPairNE => ∃' ∃' (∼(&0 =' &1)) /-- The Proposition corresponding to each field axiom -/ @[simp] @@ -72,7 +72,7 @@ def FieldAxiom.toProp (K : Type*) [Add K] [Mul K] [Neg K] [Zero K] [One K] : | .oneMul => ∀ x : K, 1 * x = x | .existsInv => ∀ x : K, x ≠ 0 → ∃ y, x * y = 1 | .leftDistrib => ∀ x y z : K, x * (y + z) = x * y + x * z - | .existsPairNe => ∃ x y : K, x ≠ y + | .existsPairNE => ∃ x y : K, x ≠ y /-- The first order theory of fields, as a theory over the language of rings -/ def _root_.FirstOrder.Language.Theory.field : Language.ring.Theory := @@ -123,7 +123,7 @@ noncomputable def fieldOfModelField (K : Type*) [Language.ring.Structure K] (dif_neg hx0).symm ▸ Classical.choose_spec (existsInv.toProp_of_model x hx0)) (dif_pos rfl) leftDistrib.toProp_of_model - existsPairNe.toProp_of_model + existsPairNE.toProp_of_model section @@ -148,7 +148,7 @@ instance [Field K] [CompatibleRing K] : Theory.field.Model K := rintro φ a rfl rw [a.realize_toSentence_iff_toProp (K := K)] cases a with - | existsPairNe => exact exists_pair_ne K + | existsPairNE => exact exists_pair_ne K | existsInv => exact fun x hx0 => ⟨x⁻¹, mul_inv_cancel hx0⟩ | addAssoc => exact add_assoc | zeroAdd => exact zero_add diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean index 2e2316a4a63e1c..8440f4100fec00 100644 --- a/Mathlib/Order/Filter/Basic.lean +++ b/Mathlib/Order/Filter/Basic.lean @@ -380,8 +380,8 @@ theorem mem_generate_iff {s : Set <| Set α} {U : Set α} : #align filter.mem_generate_iff Filter.mem_generate_iff @[simp] lemma generate_singleton (s : Set α) : generate {s} = 𝓟 s := -le_antisymm (λ _t ht ↦ mem_of_superset (mem_generate_of_mem $ mem_singleton _) ht) $ - le_generate_iff.2 $ singleton_subset_iff.2 Subset.rfl + le_antisymm (λ _t ht ↦ mem_of_superset (mem_generate_of_mem $ mem_singleton _) ht) <| + le_generate_iff.2 $ singleton_subset_iff.2 Subset.rfl /-- `mk_of_closure s hs` constructs a filter on `α` whose elements set is exactly `s : Set (Set α)`, provided one gives the assumption `hs : (generate s).sets = s`. -/ diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean index aefd93c435f072..d2a8a70182ae62 100644 --- a/Mathlib/Order/Monotone/Basic.lean +++ b/Mathlib/Order/Monotone/Basic.lean @@ -246,23 +246,23 @@ theorem monotone_dual_iff : Monotone (toDual ∘ f ∘ ofDual : αᵒᵈ → β theorem antitone_dual_iff : Antitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Antitone f := by rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff] -theorem monotone_on_dual_iff : MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s := by +theorem monotoneOn_dual_iff : MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s := by rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff] -theorem antitone_on_dual_iff : AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s := by +theorem antitoneOn_dual_iff : AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s := by rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff] -theorem strict_mono_dual_iff : StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f := by +theorem strictMono_dual_iff : StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f := by rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff] -theorem strict_anti_dual_iff : StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictAnti f := by +theorem strictAnti_dual_iff : StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictAnti f := by rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff] -theorem strict_mono_on_dual_iff : +theorem strictMonoOn_dual_iff : StrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictMonoOn f s := by rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff] -theorem strict_anti_on_dual_iff : +theorem strictAntiOn_dual_iff : StrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictAntiOn f s := by rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff] @@ -320,22 +320,22 @@ alias ⟨_, Monotone.dual⟩ := monotone_dual_iff alias ⟨_, Antitone.dual⟩ := antitone_dual_iff #align antitone.dual Antitone.dual -alias ⟨_, MonotoneOn.dual⟩ := monotone_on_dual_iff +alias ⟨_, MonotoneOn.dual⟩ := monotoneOn_dual_iff #align monotone_on.dual MonotoneOn.dual -alias ⟨_, AntitoneOn.dual⟩ := antitone_on_dual_iff +alias ⟨_, AntitoneOn.dual⟩ := antitoneOn_dual_iff #align antitone_on.dual AntitoneOn.dual -alias ⟨_, StrictMono.dual⟩ := strict_mono_dual_iff +alias ⟨_, StrictMono.dual⟩ := strictMono_dual_iff #align strict_mono.dual StrictMono.dual -alias ⟨_, StrictAnti.dual⟩ := strict_anti_dual_iff +alias ⟨_, StrictAnti.dual⟩ := strictAnti_dual_iff #align strict_anti.dual StrictAnti.dual -alias ⟨_, StrictMonoOn.dual⟩ := strict_mono_on_dual_iff +alias ⟨_, StrictMonoOn.dual⟩ := strictMonoOn_dual_iff #align strict_mono_on.dual StrictMonoOn.dual -alias ⟨_, StrictAntiOn.dual⟩ := strict_anti_on_dual_iff +alias ⟨_, StrictAntiOn.dual⟩ := strictAntiOn_dual_iff #align strict_anti_on.dual StrictAntiOn.dual end OrderDual diff --git a/Mathlib/Topology/AlexandrovDiscrete.lean b/Mathlib/Topology/AlexandrovDiscrete.lean index 6d805b1edd35c4..e26cb73c668944 100644 --- a/Mathlib/Topology/AlexandrovDiscrete.lean +++ b/Mathlib/Topology/AlexandrovDiscrete.lean @@ -62,51 +62,52 @@ variable [AlexandrovDiscrete α] {S : Set (Set α)} {f : ι → Set α} lemma isOpen_sInter : (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S) := AlexandrovDiscrete.isOpen_sInter _ lemma isOpen_iInter (hf : ∀ i, IsOpen (f i)) : IsOpen (⋂ i, f i) := -isOpen_sInter $ forall_range_iff.2 hf + isOpen_sInter $ forall_range_iff.2 hf lemma isOpen_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsOpen (f i j)) : IsOpen (⋂ i, ⋂ j, f i j) := -isOpen_iInter λ _ ↦ isOpen_iInter $ hf _ + isOpen_iInter fun _ ↦ isOpen_iInter $ hf _ lemma isClosed_sUnion (hS : ∀ s ∈ S, IsClosed s) : IsClosed (⋃₀ S) := by simp only [←isOpen_compl_iff, compl_sUnion] at hS ⊢; exact isOpen_sInter $ ball_image_iff.2 hS lemma isClosed_iUnion (hf : ∀ i, IsClosed (f i)) : IsClosed (⋃ i, f i) := -isClosed_sUnion $ forall_range_iff.2 hf + isClosed_sUnion $ forall_range_iff.2 hf lemma isClosed_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClosed (f i j)) : IsClosed (⋃ i, ⋃ j, f i j) := -isClosed_iUnion λ _ ↦ isClosed_iUnion $ hf _ + isClosed_iUnion fun _ ↦ isClosed_iUnion $ hf _ lemma isClopen_sInter (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋂₀ S) := -⟨isOpen_sInter λ s hs ↦ (hS s hs).1, isClosed_sInter λ s hs ↦ (hS s hs).2⟩ + ⟨isOpen_sInter fun s hs ↦ (hS s hs).1, isClosed_sInter fun s hs ↦ (hS s hs).2⟩ lemma isClopen_iInter (hf : ∀ i, IsClopen (f i)) : IsClopen (⋂ i, f i) := -⟨isOpen_iInter λ i ↦ (hf i).1, isClosed_iInter λ i ↦ (hf i).2⟩ + ⟨isOpen_iInter fun i ↦ (hf i).1, isClosed_iInter fun i ↦ (hf i).2⟩ lemma isClopen_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClopen (f i j)) : IsClopen (⋂ i, ⋂ j, f i j) := -isClopen_iInter λ _ ↦ isClopen_iInter $ hf _ + isClopen_iInter fun _ ↦ isClopen_iInter $ hf _ lemma isClopen_sUnion (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋃₀ S) := -⟨isOpen_sUnion λ s hs ↦ (hS s hs).1, isClosed_sUnion λ s hs ↦ (hS s hs).2⟩ + ⟨isOpen_sUnion fun s hs ↦ (hS s hs).1, isClosed_sUnion fun s hs ↦ (hS s hs).2⟩ lemma isClopen_iUnion (hf : ∀ i, IsClopen (f i)) : IsClopen (⋃ i, f i) := -⟨isOpen_iUnion λ i ↦ (hf i).1, isClosed_iUnion λ i ↦ (hf i).2⟩ + ⟨isOpen_iUnion fun i ↦ (hf i).1, isClosed_iUnion fun i ↦ (hf i).2⟩ lemma isClopen_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClopen (f i j)) : IsClopen (⋃ i, ⋃ j, f i j) := -isClopen_iUnion λ _ ↦ isClopen_iUnion $ hf _ + isClopen_iUnion fun _ ↦ isClopen_iUnion $ hf _ lemma interior_iInter (f : ι → Set α) : interior (⋂ i, f i) = ⋂ i, interior (f i) := -(interior_maximal (iInter_mono λ _ ↦ interior_subset) $ isOpen_iInter λ _ ↦ - isOpen_interior).antisymm' $ subset_iInter λ _ ↦ interior_mono $ iInter_subset _ _ + (interior_maximal (iInter_mono fun _ ↦ interior_subset) $ isOpen_iInter fun _ ↦ + isOpen_interior).antisymm' $ subset_iInter fun _ ↦ interior_mono $ iInter_subset _ _ lemma interior_sInter (S : Set (Set α)) : interior (⋂₀ S) = ⋂ s ∈ S, interior s := by simp_rw [sInter_eq_biInter, interior_iInter] lemma closure_iUnion (f : ι → Set α) : closure (⋃ i, f i) = ⋃ i, closure (f i) := - compl_injective $ by simpa only [←interior_compl, compl_iUnion] using interior_iInter λ i ↦ (f i)ᶜ + compl_injective <| by + simpa only [←interior_compl, compl_iUnion] using interior_iInter fun i ↦ (f i)ᶜ lemma closure_sUnion (S : Set (Set α)) : closure (⋃₀ S) = ⋃ s ∈ S, closure s := by simp_rw [sUnion_eq_biUnion, closure_iUnion] @@ -132,54 +133,54 @@ lemma mem_exterior : a ∈ exterior s ↔ ∀ U, IsOpen U → s ⊆ U → a ∈ lemma subset_exterior_iff : s ⊆ exterior t ↔ ∀ U, IsOpen U → t ⊆ U → s ⊆ U := by simp [exterior_def] -lemma subset_exterior : s ⊆ exterior s := subset_exterior_iff.2 $ λ _ _ ↦ id +lemma subset_exterior : s ⊆ exterior s := subset_exterior_iff.2 $ fun _ _ ↦ id lemma exterior_minimal (h₁ : s ⊆ t) (h₂ : IsOpen t) : exterior s ⊆ t := by rw [exterior_def]; exact sInter_subset_of_mem ⟨h₂, h₁⟩ lemma IsOpen.exterior_eq (h : IsOpen s) : exterior s = s := -(exterior_minimal Subset.rfl h).antisymm subset_exterior + (exterior_minimal Subset.rfl h).antisymm subset_exterior lemma IsOpen.exterior_subset_iff (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t := -⟨subset_exterior.trans, λ h ↦ exterior_minimal h ht⟩ + ⟨subset_exterior.trans, fun h ↦ exterior_minimal h ht⟩ @[mono] lemma exterior_mono : Monotone (exterior : Set α → Set α) := -λ _s _t h ↦ ker_mono $ nhdsSet_mono h + fun _s _t h ↦ ker_mono $ nhdsSet_mono h @[simp] lemma exterior_empty : exterior (∅ : Set α) = ∅ := isOpen_empty.exterior_eq @[simp] lemma exterior_univ : exterior (univ : Set α) = univ := isOpen_univ.exterior_eq @[simp] lemma exterior_eq_empty : exterior s = ∅ ↔ s = ∅ := -⟨eq_bot_mono subset_exterior, by rintro rfl; exact exterior_empty⟩ + ⟨eq_bot_mono subset_exterior, by rintro rfl; exact exterior_empty⟩ variable [AlexandrovDiscrete α] [AlexandrovDiscrete β] @[simp] lemma isOpen_exterior : IsOpen (exterior s) := by - rw [exterior_def]; exact isOpen_sInter $ λ _ ↦ And.left + rw [exterior_def]; exact isOpen_sInter $ fun _ ↦ And.left lemma exterior_mem_nhdsSet : exterior s ∈ 𝓝ˢ s := isOpen_exterior.mem_nhdsSet.2 subset_exterior @[simp] lemma exterior_eq_iff_isOpen : exterior s = s ↔ IsOpen s := - ⟨λ h ↦ h ▸ isOpen_exterior, IsOpen.exterior_eq⟩ + ⟨fun h ↦ h ▸ isOpen_exterior, IsOpen.exterior_eq⟩ @[simp] lemma exterior_subset_iff_isOpen : exterior s ⊆ s ↔ IsOpen s := by simp only [exterior_eq_iff_isOpen.symm, Subset.antisymm_iff, subset_exterior, and_true] lemma exterior_subset_iff : exterior s ⊆ t ↔ ∃ U, IsOpen U ∧ s ⊆ U ∧ U ⊆ t := - ⟨λ h ↦ ⟨exterior s, isOpen_exterior, subset_exterior, h⟩, - λ ⟨_U, hU, hsU, hUt⟩ ↦ (exterior_minimal hsU hU).trans hUt⟩ + ⟨fun h ↦ ⟨exterior s, isOpen_exterior, subset_exterior, h⟩, + fun ⟨_U, hU, hsU, hUt⟩ ↦ (exterior_minimal hsU hU).trans hUt⟩ lemma exterior_subset_iff_mem_nhdsSet : exterior s ⊆ t ↔ t ∈ 𝓝ˢ s := -exterior_subset_iff.trans mem_nhdsSet_iff_exists.symm + exterior_subset_iff.trans mem_nhdsSet_iff_exists.symm lemma exterior_singleton_subset_iff_mem_nhds : exterior {a} ⊆ t ↔ t ∈ 𝓝 a := by simp [exterior_subset_iff_mem_nhdsSet] lemma IsOpen.exterior_subset (ht : IsOpen t) : exterior s ⊆ t ↔ s ⊆ t := - ⟨subset_exterior.trans, λ h ↦ exterior_minimal h ht⟩ + ⟨subset_exterior.trans, fun h ↦ exterior_minimal h ht⟩ lemma gc_exterior_interior : GaloisConnection (exterior : Set α → Set α) interior := - λ s t ↦ by simp [exterior_subset_iff, subset_interior_iff] + fun s t ↦ by simp [exterior_subset_iff, subset_interior_iff] @[simp] lemma exterior_exterior (s : Set α) : exterior (exterior s) = exterior s := isOpen_exterior.exterior_eq @@ -194,29 +195,29 @@ lemma gc_exterior_interior : GaloisConnection (exterior : Set α → Set α) int rw [←nhdsSet_exterior, isOpen_exterior.nhdsSet_eq] @[simp] lemma exterior_subset_exterior : exterior s ⊆ exterior t ↔ 𝓝ˢ s ≤ 𝓝ˢ t := by - refine ⟨?_, λ h ↦ ker_mono h⟩ + refine ⟨?_, fun h ↦ ker_mono h⟩ simp_rw [le_def, ←exterior_subset_iff_mem_nhdsSet] - exact λ h u ↦ h.trans + exact fun h u ↦ h.trans lemma specializes_iff_exterior_subset : x ⤳ y ↔ exterior {x} ⊆ exterior {y} := by simp [Specializes] lemma isOpen_iff_forall_specializes : IsOpen s ↔ ∀ x y, x ⤳ y → y ∈ s → x ∈ s := by - refine' ⟨λ hs x y hxy ↦ hxy.mem_open hs, λ hs ↦ _⟩ + refine' ⟨fun hs x y hxy ↦ hxy.mem_open hs, fun hs ↦ _⟩ simp_rw [specializes_iff_exterior_subset] at hs simp_rw [isOpen_iff_mem_nhds, mem_nhds_iff] rintro a ha - refine ⟨_, λ b hb ↦ hs _ _ ?_ ha, isOpen_exterior, subset_exterior $ mem_singleton _⟩ + refine ⟨_, fun b hb ↦ hs _ _ ?_ ha, isOpen_exterior, subset_exterior $ mem_singleton _⟩ rwa [isOpen_exterior.exterior_subset, singleton_subset_iff] lemma Set.Finite.isCompact_exterior (hs : s.Finite) : IsCompact (exterior s) := by classical - refine isCompact_of_finite_subcover λ f hf hsf ↦ ?_ - choose g hg using λ a (ha : a ∈ exterior s) ↦ mem_iUnion.1 (hsf ha) - refine ⟨hs.toFinset.attach.image λ a ↦ g a.1 $ subset_exterior $ (Finite.mem_toFinset _).1 a.2, - (isOpen_iUnion λ i ↦ isOpen_iUnion ?_).exterior_subset.2 ?_⟩ - exact λ _ ↦ hf _ - refine λ a ha ↦ mem_iUnion₂.2 ⟨_, ?_, hg _ $ subset_exterior ha⟩ + refine isCompact_of_finite_subcover fun f hf hsf ↦ ?_ + choose g hg using fun a (ha : a ∈ exterior s) ↦ mem_iUnion.1 (hsf ha) + refine ⟨hs.toFinset.attach.image fun a ↦ g a.1 $ subset_exterior $ (Finite.mem_toFinset _).1 a.2, + (isOpen_iUnion fun i ↦ isOpen_iUnion ?_).exterior_subset.2 ?_⟩ + exact fun _ ↦ hf _ + refine fun a ha ↦ mem_iUnion₂.2 ⟨_, ?_, hg _ $ subset_exterior ha⟩ simp only [Finset.mem_image, Finset.mem_attach, true_and, Subtype.exists, Finite.mem_toFinset] exact ⟨a, ha, rfl⟩ @@ -229,19 +230,21 @@ lemma Inducing.alexandrovDiscrete {f : β → α} (h : Inducing f) : AlexandrovD lemma alexandrovDiscrete_coinduced {β : Type*} {f : α → β} : @AlexandrovDiscrete β (coinduced f ‹_›) := -@AlexandrovDiscrete.mk β (coinduced f ‹_›) λ S hS ↦ by - rw [isOpen_coinduced, preimage_sInter]; exact isOpen_iInter₂ hS + @AlexandrovDiscrete.mk β (coinduced f ‹_›) fun S hS ↦ by + rw [isOpen_coinduced, preimage_sInter]; exact isOpen_iInter₂ hS lemma AlexandrovDiscrete.sup {t₁ t₂ : TopologicalSpace α} (_ : @AlexandrovDiscrete α t₁) (_ : @AlexandrovDiscrete α t₂) : - @AlexandrovDiscrete α (t₁ ⊔ t₂) := -@AlexandrovDiscrete.mk α (t₁ ⊔ t₂) λ _S hS ↦ - ⟨@isOpen_sInter _ t₁ _ _ λ _s hs ↦ (hS _ hs).1, isOpen_sInter λ _s hs ↦ (hS _ hs).2⟩ + @AlexandrovDiscrete α (t₁ ⊔ t₂) := + @AlexandrovDiscrete.mk α (t₁ ⊔ t₂) fun _S hS ↦ + ⟨@isOpen_sInter _ t₁ _ _ fun _s hs ↦ (hS _ hs).1, isOpen_sInter fun _s hs ↦ (hS _ hs).2⟩ lemma alexandrovDiscrete_iSup {t : ι → TopologicalSpace α} (_ : ∀ i, @AlexandrovDiscrete α (t i)) : @AlexandrovDiscrete α (⨆ i, t i) := -@AlexandrovDiscrete.mk α (⨆ i, t i) λ _S hS ↦ isOpen_iSup_iff.2 λ i ↦ @isOpen_sInter _ (t i) _ _ - λ _s hs ↦ isOpen_iSup_iff.1 (hS _ hs) _ + @AlexandrovDiscrete.mk α (⨆ i, t i) + fun _S hS ↦ isOpen_iSup_iff.2 + fun i ↦ @isOpen_sInter _ (t i) _ _ + fun _s hs ↦ isOpen_iSup_iff.1 (hS _ hs) _ instance AlexandrovDiscrete.toFirstCountable : FirstCountableTopology α where nhds_generated_countable a := ⟨{exterior {a}}, countable_singleton _, by simp⟩ @@ -252,14 +255,14 @@ instance AlexandrovDiscrete.toLocallyCompactSpace : LocallyCompactSpace α where exterior_singleton_subset_iff_mem_nhds.2 hU, (finite_singleton _).isCompact_exterior⟩ instance Subtype.instAlexandrovDiscrete {p : α → Prop} : AlexandrovDiscrete {a // p a} := -inducing_subtype_val.alexandrovDiscrete + inducing_subtype_val.alexandrovDiscrete instance Quotient.instAlexandrovDiscrete {s : Setoid α} : AlexandrovDiscrete (Quotient s) := -alexandrovDiscrete_coinduced + alexandrovDiscrete_coinduced instance Sum.instAlexandrovDiscrete : AlexandrovDiscrete (α ⊕ β) := -alexandrovDiscrete_coinduced.sup alexandrovDiscrete_coinduced + alexandrovDiscrete_coinduced.sup alexandrovDiscrete_coinduced instance Sigma.instAlexandrovDiscrete {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)] - [∀ i, AlexandrovDiscrete (π i)] : AlexandrovDiscrete (Σ i, π i) := -alexandrovDiscrete_iSup λ _ ↦ alexandrovDiscrete_coinduced + [∀ i, AlexandrovDiscrete (π i)] : AlexandrovDiscrete (Σ i, π i) := + alexandrovDiscrete_iSup fun _ ↦ alexandrovDiscrete_coinduced