From 8b47b2fc9570c68ee13618220c41bf164c62061d Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 9 Jan 2024 09:25:07 +0000 Subject: [PATCH] chore(Covby): rename `Covby` to `CovBy` (#9578) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rename - `Covby` → `CovBy`, `Wcovby` → `WCovBy` - `*covby*` → `*covBy*` - `wcovby.finset_val` → `WCovBy.finset_val`, `wcovby.finset_coe` → `WCovBy.finset_coe` - `Covby.is_coatom` → `CovBy.isCoatom` --- Mathlib/Algebra/Function/Support.lean | 2 +- Mathlib/Algebra/Order/ToIntervalMod.lean | 10 +- Mathlib/Combinatorics/SetFamily/Shadow.lean | 8 +- .../SimpleGraph/ConcreteColorings.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Hasse.lean | 16 +- Mathlib/Data/Fin/FlagRange.lean | 18 +- Mathlib/Data/Finset/Grade.lean | 84 +-- Mathlib/Data/Finset/Interval.lean | 4 +- Mathlib/Data/Finset/LocallyFinite.lean | 54 +- Mathlib/Data/Int/SuccPred.lean | 26 +- Mathlib/Data/Nat/SuccPred.lean | 14 +- Mathlib/LinearAlgebra/Basis/Flag.lean | 10 +- Mathlib/LinearAlgebra/Span.lean | 10 +- Mathlib/Order/Atoms.lean | 50 +- Mathlib/Order/Cover.lean | 560 +++++++++--------- Mathlib/Order/Grade.lean | 64 +- Mathlib/Order/ModularLattice.lean | 96 +-- Mathlib/Order/SuccPred/Basic.lean | 82 +-- Mathlib/Order/SuccPred/Limit.lean | 30 +- Mathlib/RingTheory/SimpleModule.lean | 12 +- Mathlib/SetTheory/Ordinal/Topology.lean | 2 +- Mathlib/Topology/Order/Basic.lean | 26 +- Mathlib/Topology/Support.lean | 2 +- 23 files changed, 591 insertions(+), 591 deletions(-) diff --git a/Mathlib/Algebra/Function/Support.lean b/Mathlib/Algebra/Function/Support.lean index 7aa21a278e370..db6a792703cb0 100644 --- a/Mathlib/Algebra/Function/Support.lean +++ b/Mathlib/Algebra/Function/Support.lean @@ -138,7 +138,7 @@ theorem range_subset_insert_image_mulSupport (f : α → M) : @[to_additive] lemma range_eq_image_or_of_mulSupport_subset {f : α → M} {k : Set α} (h : mulSupport f ⊆ k) : range f = f '' k ∨ range f = insert 1 (f '' k) := by - apply (wcovby_insert _ _).eq_or_eq (image_subset_range _ _) + apply (wcovBy_insert _ _).eq_or_eq (image_subset_range _ _) exact (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_subset f h)) @[to_additive (attr := simp)] diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean index d5a5aed5b96c2..6702415949361 100644 --- a/Mathlib/Algebra/Order/ToIntervalMod.lean +++ b/Mathlib/Algebra/Order/ToIntervalMod.lean @@ -690,23 +690,23 @@ theorem Ico_eq_locus_Ioc_eq_iUnion_Ioo : Classical.not_not] #align Ico_eq_locus_Ioc_eq_Union_Ioo Ico_eq_locus_Ioc_eq_iUnion_Ioo -theorem toIocDiv_wcovby_toIcoDiv (a b : α) : toIocDiv hp a b ⩿ toIcoDiv hp a b := by +theorem toIocDiv_wcovBy_toIcoDiv (a b : α) : toIocDiv hp a b ⩿ toIcoDiv hp a b := by suffices toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b by - rwa [wcovby_iff_eq_or_covby, ← Order.succ_eq_iff_covby] + rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy] rw [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, ← modEq_iff_toIcoDiv_eq_toIocDiv_add_one] exact em' _ -#align to_Ioc_div_wcovby_to_Ico_div toIocDiv_wcovby_toIcoDiv +#align to_Ioc_div_wcovby_to_Ico_div toIocDiv_wcovBy_toIcoDiv theorem toIcoMod_le_toIocMod (a b : α) : toIcoMod hp a b ≤ toIocMod hp a b := by rw [toIcoMod, toIocMod, sub_le_sub_iff_left] - exact zsmul_mono_left hp.le (toIocDiv_wcovby_toIcoDiv _ _ _).le + exact zsmul_mono_left hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le #align to_Ico_mod_le_to_Ioc_mod toIcoMod_le_toIocMod theorem toIocMod_le_toIcoMod_add (a b : α) : toIocMod hp a b ≤ toIcoMod hp a b + p := by rw [toIcoMod, toIocMod, sub_add, sub_le_sub_iff_left, sub_le_iff_le_add, ← add_one_zsmul, (zsmul_strictMono_left hp).le_iff_le] - apply (toIocDiv_wcovby_toIcoDiv _ _ _).le_succ + apply (toIocDiv_wcovBy_toIcoDiv _ _ _).le_succ #align to_Ioc_mod_le_to_Ico_mod_add toIocMod_le_toIcoMod_add end IcoIoc diff --git a/Mathlib/Combinatorics/SetFamily/Shadow.lean b/Mathlib/Combinatorics/SetFamily/Shadow.lean index 31a5c219986aa..9c72b39e744c8 100644 --- a/Mathlib/Combinatorics/SetFamily/Shadow.lean +++ b/Mathlib/Combinatorics/SetFamily/Shadow.lean @@ -101,12 +101,12 @@ theorem erase_mem_shadow (hs : s ∈ 𝒜) (ha : a ∈ s) : erase s a ∈ ∂ See also `Finset.mem_shadow_iff_exists_mem_card_add_one`. -/ lemma mem_shadow_iff_exists_sdiff : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = 1 := by - simp_rw [mem_shadow_iff, ← covby_iff_card_sdiff_eq_one, covby_iff_exists_erase] + simp_rw [mem_shadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase] /-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in `𝒜`. -/ lemma mem_shadow_iff_insert_mem : t ∈ ∂ 𝒜 ↔ ∃ a, a ∉ t ∧ insert a t ∈ 𝒜 := by - simp_rw [mem_shadow_iff_exists_sdiff, ← covby_iff_card_sdiff_eq_one, covby_iff_exists_insert] + simp_rw [mem_shadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert] aesop #align finset.mem_shadow_iff_insert_mem Finset.mem_shadow_iff_insert_mem @@ -223,12 +223,12 @@ theorem insert_mem_upShadow (hs : s ∈ 𝒜) (ha : a ∉ s) : insert a s ∈ See also `Finset.mem_upShadow_iff_exists_mem_card_add_one`. -/ lemma mem_upShadow_iff_exists_sdiff : t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = 1 := by - simp_rw [mem_upShadow_iff, ← covby_iff_card_sdiff_eq_one, covby_iff_exists_insert] + simp_rw [mem_upShadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert] /-- `t` is in the upper shadow of `𝒜` iff we can remove an element from it so that the resulting finset is in `𝒜`. -/ lemma mem_upShadow_iff_erase_mem : t ∈ ∂⁺ 𝒜 ↔ ∃ a, a ∈ t ∧ erase t a ∈ 𝒜 := by - simp_rw [mem_upShadow_iff_exists_sdiff, ← covby_iff_card_sdiff_eq_one, covby_iff_exists_erase] + simp_rw [mem_upShadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase] aesop #align finset.mem_up_shadow_iff_erase_mem Finset.mem_upShadow_iff_erase_mem diff --git a/Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean b/Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean index 4cd23b04915e2..58ea1459db13f 100644 --- a/Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean +++ b/Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean @@ -38,7 +38,7 @@ def pathGraph_two_embedding (n : ℕ) (h : 2 ≤ n) : pathGraph 2 ↪g pathGraph exact Fin.ext map_rel_iff' := by intro v w - fin_cases v <;> fin_cases w <;> simp [pathGraph, ← Fin.coe_covby_iff] + fin_cases v <;> fin_cases w <;> simp [pathGraph, ← Fin.coe_covBy_iff] theorem chromaticNumber_pathGraph (n : ℕ) (h : 2 ≤ n) : (pathGraph n).chromaticNumber = 2 := by diff --git a/Mathlib/Combinatorics/SimpleGraph/Hasse.lean b/Mathlib/Combinatorics/SimpleGraph/Hasse.lean index 5a7d715f64431..f4a4956015ba1 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Hasse.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Hasse.lean @@ -13,7 +13,7 @@ import Mathlib.Order.SuccPred.Relation /-! # The Hasse diagram as a graph -This file defines the Hasse diagram of an order (graph of `Covby`, the covering relation) and the +This file defines the Hasse diagram of an order (graph of `CovBy`, the covering relation) and the path graph on `n` vertices. ## Main declarations @@ -71,7 +71,7 @@ variable [PartialOrder α] [PartialOrder β] @[simp] theorem hasse_prod : hasse (α × β) = hasse α □ hasse β := by ext x y - simp_rw [boxProd_adj, hasse_adj, Prod.covby_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2, + simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2, or_or_or_comm] #align simple_graph.hasse_prod SimpleGraph.hasse_prod @@ -85,16 +85,16 @@ theorem hasse_preconnected_of_succ [SuccOrder α] [IsSuccArchimedean α] : (hass fun a b => by rw [reachable_iff_reflTransGen] exact - reflTransGen_of_succ _ (fun c hc => Or.inl <| covby_succ_of_not_isMax hc.2.not_isMax) - fun c hc => Or.inr <| covby_succ_of_not_isMax hc.2.not_isMax + reflTransGen_of_succ _ (fun c hc => Or.inl <| covBy_succ_of_not_isMax hc.2.not_isMax) + fun c hc => Or.inr <| covBy_succ_of_not_isMax hc.2.not_isMax #align simple_graph.hasse_preconnected_of_succ SimpleGraph.hasse_preconnected_of_succ theorem hasse_preconnected_of_pred [PredOrder α] [IsPredArchimedean α] : (hasse α).Preconnected := fun a b => by rw [reachable_iff_reflTransGen, ← reflTransGen_swap] exact - reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covby_of_not_isMin hc.1.not_isMin) - fun c hc => Or.inr <| pred_covby_of_not_isMin hc.1.not_isMin + reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covBy_of_not_isMin hc.1.not_isMin) + fun c hc => Or.inr <| pred_covBy_of_not_isMin hc.1.not_isMin #align simple_graph.hasse_preconnected_of_pred SimpleGraph.hasse_preconnected_of_pred end LinearOrder @@ -107,7 +107,7 @@ def pathGraph (n : ℕ) : SimpleGraph (Fin n) := theorem pathGraph_adj {n : ℕ} {u v : Fin n} : (pathGraph n).Adj u v ↔ u.val + 1 = v.val ∨ v.val + 1 = u.val := by simp only [pathGraph, hasse] - simp_rw [← Fin.coe_covby_iff, Nat.covby_iff_succ_eq] + simp_rw [← Fin.coe_covBy_iff, Nat.covBy_iff_succ_eq] theorem pathGraph_preconnected (n : ℕ) : (pathGraph n).Preconnected := hasse_preconnected_of_succ _ @@ -119,6 +119,6 @@ theorem pathGraph_connected (n : ℕ) : (pathGraph (n + 1)).Connected := theorem pathGraph_two_eq_top : pathGraph 2 = ⊤ := by ext u v - fin_cases u <;> fin_cases v <;> simp [pathGraph, ← Fin.coe_covby_iff, Nat.covby_iff_succ_eq] + fin_cases u <;> fin_cases v <;> simp [pathGraph, ← Fin.coe_covBy_iff, Nat.covBy_iff_succ_eq] end SimpleGraph diff --git a/Mathlib/Data/Fin/FlagRange.lean b/Mathlib/Data/Fin/FlagRange.lean index 6d2f96ee9c456..17082ff70e88a 100644 --- a/Mathlib/Data/Fin/FlagRange.lean +++ b/Mathlib/Data/Fin/FlagRange.lean @@ -28,10 +28,10 @@ variable {α : Type*} [PartialOrder α] [BoundedOrder α] {n : ℕ} {f : Fin (n - `fₖ₊₁` weakly covers `fₖ` for all `0 ≤ k < n`; this means that `fₖ ≤ fₖ₊₁` and there is no `c` such that `fₖ simpa [h0, bot_lt_iff_ne_bot] using (h 0).symm | succ k ihk => rw [range_subset_iff] at hbt - exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovby k).2 ihk) + exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk) /-- Let `f : Fin (n + 1) → α` be an `(n + 1)`-tuple `(f₀, …, fₙ)` such that - `f₀ = ⊥` and `fₙ = ⊤`; @@ -49,11 +49,11 @@ theorem IsMaxChain.range_fin_of_covby (h0 : f 0 = ⊥) (hlast : f (.last n) = Then the range of `f` is a `Flag α`. -/ @[simps] def Flag.rangeFin (f : Fin (n + 1) → α) (h0 : f 0 = ⊥) (hlast : f (.last n) = ⊤) - (hcovby : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) : Flag α where + (hcovBy : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) : Flag α where carrier := range f - Chain' := (IsMaxChain.range_fin_of_covby h0 hlast hcovby).1 - max_chain' := (IsMaxChain.range_fin_of_covby h0 hlast hcovby).2 + Chain' := (IsMaxChain.range_fin_of_covBy h0 hlast hcovBy).1 + max_chain' := (IsMaxChain.range_fin_of_covBy h0 hlast hcovBy).2 -@[simp] theorem Flag.mem_rangeFin {x h0 hlast hcovby} : - x ∈ rangeFin f h0 hlast hcovby ↔ ∃ k, f k = x := +@[simp] theorem Flag.mem_rangeFin {x h0 hlast hcovBy} : + x ∈ rangeFin f h0 hlast hcovBy ↔ ∃ k, f k = x := Iff.rfl diff --git a/Mathlib/Data/Finset/Grade.lean b/Mathlib/Data/Finset/Grade.lean index af6cc83e1f924..4c5c5fc907f85 100644 --- a/Mathlib/Data/Finset/Grade.lean +++ b/Mathlib/Data/Finset/Grade.lean @@ -27,27 +27,27 @@ variable {α : Type*} namespace Multiset variable {s t : Multiset α} {a : α} -@[simp] lemma covby_cons (s : Multiset α) (a : α) : s ⋖ a ::ₘ s := - ⟨lt_cons_self _ _, fun t hst hts ↦ (covby_succ _).2 (card_lt_card hst) <| by +@[simp] lemma covBy_cons (s : Multiset α) (a : α) : s ⋖ a ::ₘ s := + ⟨lt_cons_self _ _, fun t hst hts ↦ (covBy_succ _).2 (card_lt_card hst) <| by simpa using card_lt_card hts⟩ -lemma _root_.Covby.exists_multiset_cons (h : s ⋖ t) : ∃ a, a ::ₘ s = t := +lemma _root_.CovBy.exists_multiset_cons (h : s ⋖ t) : ∃ a, a ::ₘ s = t := (lt_iff_cons_le.1 h.lt).imp fun _a ha ↦ ha.eq_of_not_lt <| h.2 <| lt_cons_self _ _ -lemma covby_iff : s ⋖ t ↔ ∃ a, a ::ₘ s = t := - ⟨Covby.exists_multiset_cons, by rintro ⟨a, rfl⟩; exact covby_cons _ _⟩ +lemma covBy_iff : s ⋖ t ↔ ∃ a, a ::ₘ s = t := + ⟨CovBy.exists_multiset_cons, by rintro ⟨a, rfl⟩; exact covBy_cons _ _⟩ -lemma _root_.Covby.card_multiset (h : s ⋖ t) : card s ⋖ card t := by - obtain ⟨a, rfl⟩ := h.exists_multiset_cons; rw [card_cons]; exact covby_succ _ +lemma _root_.CovBy.card_multiset (h : s ⋖ t) : card s ⋖ card t := by + obtain ⟨a, rfl⟩ := h.exists_multiset_cons; rw [card_cons]; exact covBy_succ _ -lemma isAtom_iff : IsAtom s ↔ ∃ a, s = {a} := by simp [← bot_covby_iff, covby_iff, eq_comm] +lemma isAtom_iff : IsAtom s ↔ ∃ a, s = {a} := by simp [← bot_covBy_iff, covBy_iff, eq_comm] @[simp] lemma isAtom_singleton (a : α) : IsAtom ({a} : Multiset α) := isAtom_iff.2 ⟨_, rfl⟩ instance instGradeMinOrder : GradeMinOrder ℕ (Multiset α) where grade := card grade_strictMono := card_strictMono - covby_grade s t := Covby.card_multiset + covBy_grade s t := CovBy.card_multiset isMin_grade s hs := by rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot @[simp] lemma grade_eq (m : Multiset α) : grade ℕ m = card m := rfl @@ -65,56 +65,56 @@ lemma ordConnected_range_val : Set.OrdConnected (Set.range val : Set <| Multiset lemma ordConnected_range_coe : Set.OrdConnected (Set.range ((↑) : Finset α → Set α)) := ⟨by rintro _ _ _ ⟨s, rfl⟩ t ht; exact ⟨_, (s.finite_toSet.subset ht.2).coe_toFinset⟩⟩ -@[simp] lemma val_wcovby_val : s.1 ⩿ t.1 ↔ s ⩿ t := - ordConnected_range_val.apply_wcovby_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩ +@[simp] lemma val_wcovBy_val : s.1 ⩿ t.1 ↔ s ⩿ t := + ordConnected_range_val.apply_wcovBy_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩ -@[simp] lemma val_covby_val : s.1 ⋖ t.1 ↔ s ⋖ t := - ordConnected_range_val.apply_covby_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩ +@[simp] lemma val_covBy_val : s.1 ⋖ t.1 ↔ s ⋖ t := + ordConnected_range_val.apply_covBy_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩ -@[simp] lemma coe_wcovby_coe : (s : Set α) ⩿ t ↔ s ⩿ t := - ordConnected_range_coe.apply_wcovby_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩ +@[simp] lemma coe_wcovBy_coe : (s : Set α) ⩿ t ↔ s ⩿ t := + ordConnected_range_coe.apply_wcovBy_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩ -@[simp] lemma coe_covby_coe : (s : Set α) ⋖ t ↔ s ⋖ t := - ordConnected_range_coe.apply_covby_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩ +@[simp] lemma coe_covBy_coe : (s : Set α) ⋖ t ↔ s ⋖ t := + ordConnected_range_coe.apply_covBy_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩ -alias ⟨_, _root_.wcovby.finset_val⟩ := val_wcovby_val -alias ⟨_, _root_.Covby.finset_val⟩ := val_covby_val -alias ⟨_, _root_.wcovby.finset_coe⟩ := coe_wcovby_coe -alias ⟨_, _root_.Covby.finset_coe⟩ := coe_covby_coe +alias ⟨_, _root_.WCovBy.finset_val⟩ := val_wcovBy_val +alias ⟨_, _root_.CovBy.finset_val⟩ := val_covBy_val +alias ⟨_, _root_.WCovBy.finset_coe⟩ := coe_wcovBy_coe +alias ⟨_, _root_.CovBy.finset_coe⟩ := coe_covBy_coe -@[simp] lemma covby_cons (ha : a ∉ s) : s ⋖ s.cons a ha := by simp [← val_covby_val] +@[simp] lemma covBy_cons (ha : a ∉ s) : s ⋖ s.cons a ha := by simp [← val_covBy_val] -lemma _root_.Covby.exists_finset_cons (h : s ⋖ t) : ∃ a, ∃ ha : a ∉ s, s.cons a ha = t := +lemma _root_.CovBy.exists_finset_cons (h : s ⋖ t) : ∃ a, ∃ ha : a ∉ s, s.cons a ha = t := let ⟨a, ha, hst⟩ := ssubset_iff_exists_cons_subset.1 h.lt ⟨a, ha, (hst.eq_of_not_ssuperset <| h.2 <| ssubset_cons _).symm⟩ -lemma covby_iff_exists_cons : s ⋖ t ↔ ∃ a, ∃ ha : a ∉ s, s.cons a ha = t := - ⟨Covby.exists_finset_cons, by rintro ⟨a, ha, rfl⟩; exact covby_cons _⟩ +lemma covBy_iff_exists_cons : s ⋖ t ↔ ∃ a, ∃ ha : a ∉ s, s.cons a ha = t := + ⟨CovBy.exists_finset_cons, by rintro ⟨a, ha, rfl⟩; exact covBy_cons _⟩ -lemma _root_.Covby.card_finset (h : s ⋖ t) : s.card ⋖ t.card := (val_covby_val.2 h).card_multiset +lemma _root_.CovBy.card_finset (h : s ⋖ t) : s.card ⋖ t.card := (val_covBy_val.2 h).card_multiset section DecidableEq variable [DecidableEq α] -@[simp] lemma wcovby_insert (s : Finset α) (a : α) : s ⩿ insert a s := by simp [← coe_wcovby_coe] -@[simp] lemma erase_wcovby (s : Finset α) (a : α) : s.erase a ⩿ s := by simp [← coe_wcovby_coe] +@[simp] lemma wcovBy_insert (s : Finset α) (a : α) : s ⩿ insert a s := by simp [← coe_wcovBy_coe] +@[simp] lemma erase_wcovBy (s : Finset α) (a : α) : s.erase a ⩿ s := by simp [← coe_wcovBy_coe] -lemma covby_insert (ha : a ∉ s) : s ⋖ insert a s := - (wcovby_insert _ _).covby_of_lt <| ssubset_insert ha +lemma covBy_insert (ha : a ∉ s) : s ⋖ insert a s := + (wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha -@[simp] lemma erase_covby (ha : a ∈ s) : s.erase a ⋖ s := ⟨erase_ssubset ha, (erase_wcovby _ _).2⟩ +@[simp] lemma erase_covBy (ha : a ∈ s) : s.erase a ⋖ s := ⟨erase_ssubset ha, (erase_wcovBy _ _).2⟩ -lemma _root_.Covby.exists_finset_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t := by +lemma _root_.CovBy.exists_finset_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t := by simpa using h.exists_finset_cons -lemma _root_.Covby.exists_finset_erase (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s := by +lemma _root_.CovBy.exists_finset_erase (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s := by simpa only [← coe_inj, coe_erase] using h.finset_coe.exists_set_sdiff_singleton -lemma covby_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t := by - simp only [← coe_covby_coe, Set.covby_iff_exists_insert, ← coe_inj, coe_insert, mem_coe] +lemma covBy_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t := by + simp only [← coe_covBy_coe, Set.covBy_iff_exists_insert, ← coe_inj, coe_insert, mem_coe] -lemma covby_iff_card_sdiff_eq_one : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1 := by - rw [covby_iff_exists_insert] +lemma covBy_iff_card_sdiff_eq_one : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1 := by + rw [covBy_iff_exists_insert] constructor · rintro ⟨a, ha, rfl⟩ simp [*] @@ -123,8 +123,8 @@ lemma covby_iff_card_sdiff_eq_one : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1 := refine ⟨a, (mem_sdiff.1 <| superset_of_eq ha <| mem_singleton_self _).2, ?_⟩ rw [insert_eq, ← ha, sdiff_union_of_subset hts] -lemma covby_iff_exists_erase : s ⋖ t ↔ ∃ a ∈ t, t.erase a = s := by - simp only [← coe_covby_coe, Set.covby_iff_exists_sdiff_singleton, ← coe_inj, coe_erase, mem_coe] +lemma covBy_iff_exists_erase : s ⋖ t ↔ ∃ a ∈ t, t.erase a = s := by + simp only [← coe_covBy_coe, Set.covBy_iff_exists_sdiff_singleton, ← coe_inj, coe_erase, mem_coe] end DecidableEq @@ -132,7 +132,7 @@ end DecidableEq ⟨singleton_ne_empty a, fun _ ↦ eq_empty_of_ssubset_singleton⟩ protected lemma isAtom_iff : IsAtom s ↔ ∃ a, s = {a} := by - simp [← bot_covby_iff, covby_iff_exists_cons, eq_comm] + simp [← bot_covBy_iff, covBy_iff_exists_cons, eq_comm] section Fintype variable [Fintype α] [DecidableEq α] @@ -149,7 +149,7 @@ to record that the inclusion `Finset α ↪ Multiset α` preserves the covering instance instGradeMinOrder_multiset : GradeMinOrder (Multiset α) (Finset α) where grade := val grade_strictMono := val_strictMono - covby_grade _ _ := Covby.finset_val + covBy_grade _ _ := CovBy.finset_val isMin_grade s hs := by rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot @[simp] lemma grade_multiset_eq (s : Finset α) : grade (Multiset α) s = s.1 := rfl @@ -157,7 +157,7 @@ instance instGradeMinOrder_multiset : GradeMinOrder (Multiset α) (Finset α) wh instance instGradeMinOrder_nat : GradeMinOrder ℕ (Finset α) where grade := card grade_strictMono := card_strictMono - covby_grade _ _ := Covby.card_finset + covBy_grade _ _ := CovBy.card_finset isMin_grade s hs := by rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot @[simp] lemma grade_eq (s : Finset α) : grade ℕ s = s.card := rfl diff --git a/Mathlib/Data/Finset/Interval.lean b/Mathlib/Data/Finset/Interval.lean index dddeb3e61d7be..9c787cd92a468 100644 --- a/Mathlib/Data/Finset/Interval.lean +++ b/Mathlib/Data/Finset/Interval.lean @@ -140,7 +140,7 @@ section Cons /-- A function `f` from `Finset α` is monotone if and only if `f s ≤ f (cons a s ha)` for all `s` and `a ∉ s`. -/ lemma monotone_iff_forall_le_cons : Monotone f ↔ ∀ s, ∀ ⦃a⦄ (ha), f s ≤ f (cons a s ha) := by - classical simp [monotone_iff_forall_covby, covby_iff_exists_cons] + classical simp [monotone_iff_forall_covBy, covBy_iff_exists_cons] /-- A function `f` from `Finset α` is antitone if and only if `f (cons a s ha) ≤ f s` for all `s` and `a ∉ s`. -/ @@ -150,7 +150,7 @@ lemma antitone_iff_forall_cons_le : Antitone f ↔ ∀ s ⦃a⦄ ha, f (cons a s /-- A function `f` from `Finset α` is strictly monotone if and only if `f s < f (cons a s ha)` for all `s` and `a ∉ s`. -/ lemma strictMono_iff_forall_lt_cons : StrictMono f ↔ ∀ s ⦃a⦄ ha, f s < f (cons a s ha) := by - classical simp [strictMono_iff_forall_covby, covby_iff_exists_cons] + classical simp [strictMono_iff_forall_covBy, covBy_iff_exists_cons] /-- A function `f` from `Finset α` is strictly antitone if and only if `f (cons a s ha) < f s` for all `s` and `a ∉ s`. -/ diff --git a/Mathlib/Data/Finset/LocallyFinite.lean b/Mathlib/Data/Finset/LocallyFinite.lean index f0293ee9a027f..e67d40a31392e 100644 --- a/Mathlib/Data/Finset/LocallyFinite.lean +++ b/Mathlib/Data/Finset/LocallyFinite.lean @@ -19,10 +19,10 @@ In addition, it shows that in a locally finite order `≤` and `<` are the trans respectively, `⩿` and `⋖`, which then leads to a characterization of monotone and strictly functions whose domain is a locally finite order. In particular, this file proves: -* `le_iff_transGen_wcovby`: `≤` is the transitive closure of `⩿` -* `lt_iff_transGen_covby`: `≤` is the transitive closure of `⩿` -* `monotone_iff_forall_wcovby`: Characterization of monotone functions -* `strictMono_iff_forall_covby`: Characterization of strictly monotone functions +* `le_iff_transGen_wcovBy`: `≤` is the transitive closure of `⩿` +* `lt_iff_transGen_covBy`: `≤` is the transitive closure of `⩿` +* `monotone_iff_forall_wcovBy`: Characterization of monotone functions +* `strictMono_iff_forall_covBy`: Characterization of strictly monotone functions ## TODO @@ -1192,7 +1192,7 @@ section Cover open Finset Relation set_option linter.unusedVariables false in -- `have` for wf induction triggers linter -lemma transGen_wcovby_of_le [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x ≤ y) : +lemma transGen_wcovBy_of_le [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x ≤ y) : TransGen (· ⩿ ·) x y := by -- We proceed by well-founded induction on the cardinality of `Icc x y`. -- It's impossible for the cardinality to be zero since `x ≤ y` @@ -1200,7 +1200,7 @@ lemma transGen_wcovby_of_le [Preorder α] [LocallyFiniteOrder α] {x y : α} (hx ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_not_mem_Ico⟩⟩⟩ by_cases hxy' : y ≤ x -- If `y ≤ x`, then `x ⩿ y` - · exact .single <| wcovby_of_le_of_le hxy hxy' + · exact .single <| wcovBy_of_le_of_le hxy hxy' /- and if `¬ y ≤ x`, then `x < y`, not because it is a linear order, but because `x ≤ y` already. In that case, since `z` is maximal in `Ico x y`, then `z ⩿ y` and we can use the induction hypothesis to show that `Relation.TransGen (· ⩿ ·) x z`. -/ @@ -1210,7 +1210,7 @@ lemma transGen_wcovby_of_le [Preorder α] [LocallyFiniteOrder α] {x y : α} (hx (Icc x z).card ≤ (Ico x y).card := card_le_card <| Icc_subset_Ico_right (mem_Ico.mp z_mem).2 _ < (Icc x y).card := this - have h₁ := transGen_wcovby_of_le (mem_Ico.mp z_mem).1 + have h₁ := transGen_wcovBy_of_le (mem_Ico.mp z_mem).1 have h₂ : z ⩿ y := by refine ⟨(mem_Ico.mp z_mem).2.le, fun c hzc hcy ↦ hz c ?_ hzc⟩ exact mem_Ico.mpr <| ⟨(mem_Ico.mp z_mem).1.trans hzc.le, hcy⟩ @@ -1218,20 +1218,20 @@ lemma transGen_wcovby_of_le [Preorder α] [LocallyFiniteOrder α] {x y : α} (hx termination_by _ => (Icc x y).card /-- In a locally finite preorder, `≤` is the transitive closure of `⩿`. -/ -lemma le_iff_transGen_wcovby [Preorder α] [LocallyFiniteOrder α] {x y : α} : +lemma le_iff_transGen_wcovBy [Preorder α] [LocallyFiniteOrder α] {x y : α} : x ≤ y ↔ TransGen (· ⩿ ·) x y := by - refine ⟨transGen_wcovby_of_le, fun h ↦ ?_⟩ + refine ⟨transGen_wcovBy_of_le, fun h ↦ ?_⟩ induction h with | single h => exact h.le | tail _ h₁ h₂ => exact h₂.trans h₁.le /-- In a locally finite partial order, `≤` is the reflexive transitive closure of `⋖`. -/ -lemma le_iff_reflTransGen_covby [PartialOrder α] [LocallyFiniteOrder α] {x y : α} : +lemma le_iff_reflTransGen_covBy [PartialOrder α] [LocallyFiniteOrder α] {x y : α} : x ≤ y ↔ ReflTransGen (· ⋖ ·) x y := by - rw [le_iff_transGen_wcovby, wcovby_eq_reflGen_covby, transGen_reflGen] + rw [le_iff_transGen_wcovBy, wcovBy_eq_reflGen_covBy, transGen_reflGen] set_option linter.unusedVariables false in -- `have` for wf induction triggers linter -lemma transGen_covby_of_lt [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x < y) : +lemma transGen_covBy_of_lt [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x < y) : TransGen (· ⋖ ·) x y := by -- We proceed by well-founded induction on the cardinality of `Ico x y`. -- It's impossible for the cardinality to be zero since `x < y` @@ -1248,7 +1248,7 @@ lemma transGen_covby_of_lt [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy by_cases hxz : x < z /- when `x < z`, then we may use the induction hypothesis to get a chain `Relation.TransGen (· ⋖ ·) x z`, which we can extend with `Relation.TransGen.tail`. -/ - · exact .tail (transGen_covby_of_lt hxz) hzy + · exact .tail (transGen_covBy_of_lt hxz) hzy /- when `¬ x < z`, then actually `z ≤ x` (not because it's a linear order, but because `x ≤ z`), and since `z ⋖ y` we conclude that `x ⋖ y` , then `Relation.TransGen.single`. -/ · simp only [lt_iff_le_not_le, not_and, not_not] at hxz @@ -1256,9 +1256,9 @@ lemma transGen_covby_of_lt [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy termination_by _ => (Ico x y).card /-- In a locally finite preorder, `<` is the transitive closure of `⋖`. -/ -lemma lt_iff_transGen_covby [Preorder α] [LocallyFiniteOrder α] {x y : α} : +lemma lt_iff_transGen_covBy [Preorder α] [LocallyFiniteOrder α] {x y : α} : x < y ↔ TransGen (· ⋖ ·) x y := by - refine ⟨transGen_covby_of_lt, fun h ↦ ?_⟩ + refine ⟨transGen_covBy_of_lt, fun h ↦ ?_⟩ induction h with | single hx => exact hx.1 | tail _ hb ih => exact ih.trans hb.1 @@ -1267,45 +1267,45 @@ variable {β : Type*} /-- A function from a locally finite preorder is monotone if and only if it is monotone when restricted to pairs satisfying `a ⩿ b`. -/ -lemma monotone_iff_forall_wcovby [Preorder α] [LocallyFiniteOrder α] [Preorder β] +lemma monotone_iff_forall_wcovBy [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : Monotone f ↔ ∀ a b : α, a ⩿ b → f a ≤ f b := by refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩ simpa [transGen_eq_self (r := ((· : β) ≤ ·)) transitive_le] - using TransGen.lift f h <| le_iff_transGen_wcovby.mp hab + using TransGen.lift f h <| le_iff_transGen_wcovBy.mp hab /-- A function from a locally finite partial order is monotone if and only if it is monotone when restricted to pairs satisfying `a ⋖ b`. -/ -lemma monotone_iff_forall_covby [PartialOrder α] [LocallyFiniteOrder α] [Preorder β] +lemma monotone_iff_forall_covBy [PartialOrder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : Monotone f ↔ ∀ a b : α, a ⋖ b → f a ≤ f b := by refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩ simpa [reflTransGen_eq_self (r := ((· : β) ≤ ·)) IsRefl.reflexive transitive_le] - using ReflTransGen.lift f h <| le_iff_reflTransGen_covby.mp hab + using ReflTransGen.lift f h <| le_iff_reflTransGen_covBy.mp hab /-- A function from a locally finite preorder is strictly monotone if and only if it is strictly monotone when restricted to pairs satisfying `a ⋖ b`. -/ -lemma strictMono_iff_forall_covby [Preorder α] [LocallyFiniteOrder α] [Preorder β] +lemma strictMono_iff_forall_covBy [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : StrictMono f ↔ ∀ a b : α, a ⋖ b → f a < f b := by refine ⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩ have := Relation.TransGen.lift f h (a := a) (b := b) - rw [← lt_iff_transGen_covby, transGen_eq_self (@lt_trans β _)] at this + rw [← lt_iff_transGen_covBy, transGen_eq_self (@lt_trans β _)] at this · exact this hab /-- A function from a locally finite preorder is antitone if and only if it is antitone when restricted to pairs satisfying `a ⩿ b`. -/ -lemma antitone_iff_forall_wcovby [Preorder α] [LocallyFiniteOrder α] [Preorder β] +lemma antitone_iff_forall_wcovBy [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : Antitone f ↔ ∀ a b : α, a ⩿ b → f b ≤ f a := - monotone_iff_forall_wcovby (β := βᵒᵈ) f + monotone_iff_forall_wcovBy (β := βᵒᵈ) f /-- A function from a locally finite partial order is antitone if and only if it is antitone when restricted to pairs satisfying `a ⋖ b`. -/ -lemma antitone_iff_forall_covby [PartialOrder α] [LocallyFiniteOrder α] [Preorder β] +lemma antitone_iff_forall_covBy [PartialOrder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : Antitone f ↔ ∀ a b : α, a ⋖ b → f b ≤ f a := - monotone_iff_forall_covby (β := βᵒᵈ) f + monotone_iff_forall_covBy (β := βᵒᵈ) f /-- A function from a locally finite preorder is strictly antitone if and only if it is strictly antitone when restricted to pairs satisfying `a ⋖ b`. -/ -lemma strictAnti_iff_forall_covby [Preorder α] [LocallyFiniteOrder α] [Preorder β] +lemma strictAnti_iff_forall_covBy [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : StrictAnti f ↔ ∀ a b : α, a ⋖ b → f b < f a := - strictMono_iff_forall_covby (β := βᵒᵈ) f + strictMono_iff_forall_covBy (β := βᵒᵈ) f end Cover diff --git a/Mathlib/Data/Int/SuccPred.lean b/Mathlib/Data/Int/SuccPred.lean index a54db0d57a2d6..0b39e3cbe3b87 100644 --- a/Mathlib/Data/Int/SuccPred.lean +++ b/Mathlib/Data/Int/SuccPred.lean @@ -73,26 +73,26 @@ instance : IsPredArchimedean ℤ := /-! ### Covering relation -/ -protected theorem covby_iff_succ_eq {m n : ℤ} : m ⋖ n ↔ m + 1 = n := - succ_eq_iff_covby.symm -#align int.covby_iff_succ_eq Int.covby_iff_succ_eq +protected theorem covBy_iff_succ_eq {m n : ℤ} : m ⋖ n ↔ m + 1 = n := + succ_eq_iff_covBy.symm +#align int.covby_iff_succ_eq Int.covBy_iff_succ_eq @[simp] -theorem sub_one_covby (z : ℤ) : z - 1 ⋖ z := by rw [Int.covby_iff_succ_eq, sub_add_cancel] -#align int.sub_one_covby Int.sub_one_covby +theorem sub_one_covBy (z : ℤ) : z - 1 ⋖ z := by rw [Int.covBy_iff_succ_eq, sub_add_cancel] +#align int.sub_one_covby Int.sub_one_covBy @[simp] -theorem covby_add_one (z : ℤ) : z ⋖ z + 1 := - Int.covby_iff_succ_eq.mpr rfl -#align int.covby_add_one Int.covby_add_one +theorem covBy_add_one (z : ℤ) : z ⋖ z + 1 := + Int.covBy_iff_succ_eq.mpr rfl +#align int.covby_add_one Int.covBy_add_one end Int @[simp, norm_cast] -theorem Nat.cast_int_covby_iff {a b : ℕ} : (a : ℤ) ⋖ b ↔ a ⋖ b := by - rw [Nat.covby_iff_succ_eq, Int.covby_iff_succ_eq] +theorem Nat.cast_int_covBy_iff {a b : ℕ} : (a : ℤ) ⋖ b ↔ a ⋖ b := by + rw [Nat.covBy_iff_succ_eq, Int.covBy_iff_succ_eq] exact Int.coe_nat_inj' -#align nat.cast_int_covby_iff Nat.cast_int_covby_iff +#align nat.cast_int_covby_iff Nat.cast_int_covBy_iff -alias ⟨_, Covby.cast_int⟩ := Nat.cast_int_covby_iff -#align covby.cast_int Covby.cast_int +alias ⟨_, CovBy.cast_int⟩ := Nat.cast_int_covBy_iff +#align covby.cast_int CovBy.cast_int diff --git a/Mathlib/Data/Nat/SuccPred.lean b/Mathlib/Data/Nat/SuccPred.lean index d937d70d353eb..21813f92c9443 100644 --- a/Mathlib/Data/Nat/SuccPred.lean +++ b/Mathlib/Data/Nat/SuccPred.lean @@ -79,16 +79,16 @@ lemma forall_ne_zero_iff (P : ℕ → Prop) : /-! ### Covering relation -/ -protected theorem covby_iff_succ_eq {m n : ℕ} : m ⋖ n ↔ m + 1 = n := - succ_eq_iff_covby.symm -#align nat.covby_iff_succ_eq Nat.covby_iff_succ_eq +protected theorem covBy_iff_succ_eq {m n : ℕ} : m ⋖ n ↔ m + 1 = n := + succ_eq_iff_covBy.symm +#align nat.covby_iff_succ_eq Nat.covBy_iff_succ_eq end Nat @[simp, norm_cast] -theorem Fin.coe_covby_iff {n : ℕ} {a b : Fin n} : (a : ℕ) ⋖ b ↔ a ⋖ b := +theorem Fin.coe_covBy_iff {n : ℕ} {a b : Fin n} : (a : ℕ) ⋖ b ↔ a ⋖ b := and_congr_right' ⟨fun h _c hc => h hc, fun h c ha hb => @h ⟨c, hb.trans b.prop⟩ ha hb⟩ -#align fin.coe_covby_iff Fin.coe_covby_iff +#align fin.coe_covby_iff Fin.coe_covBy_iff -alias ⟨_, Covby.coe_fin⟩ := Fin.coe_covby_iff -#align covby.coe_fin Covby.coe_fin +alias ⟨_, CovBy.coe_fin⟩ := Fin.coe_covBy_iff +#align covby.coe_fin CovBy.coe_fin diff --git a/Mathlib/LinearAlgebra/Basis/Flag.lean b/Mathlib/LinearAlgebra/Basis/Flag.lean index 646ed7fa109b7..6ae87d009929c 100644 --- a/Mathlib/LinearAlgebra/Basis/Flag.lean +++ b/Mathlib/LinearAlgebra/Basis/Flag.lean @@ -85,20 +85,20 @@ section DivisionRing variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} -theorem flag_covby (b : Basis (Fin n) K V) (i : Fin n) : +theorem flag_covBy (b : Basis (Fin n) K V) (i : Fin n) : b.flag i.castSucc ⋖ b.flag i.succ := by rw [flag_succ] - apply covby_span_singleton_sup + apply covBy_span_singleton_sup simp -theorem flag_wcovby (b : Basis (Fin n) K V) (i : Fin n) : +theorem flag_wcovBy (b : Basis (Fin n) K V) (i : Fin n) : b.flag i.castSucc ⩿ b.flag i.succ := - (b.flag_covby i).wcovby + (b.flag_covBy i).wcovBy /-- Range of `Basis.flag` as a `Flag`. -/ @[simps!] def toFlag (b : Basis (Fin n) K V) : Flag (Submodule K V) := - .rangeFin b.flag b.flag_zero b.flag_last b.flag_wcovby + .rangeFin b.flag b.flag_zero b.flag_last b.flag_wcovBy @[simp] theorem mem_toFlag (b : Basis (Fin n) K V) {p : Submodule K V} : p ∈ b.toFlag ↔ ∃ k, b.flag k = p := diff --git a/Mathlib/LinearAlgebra/Span.lean b/Mathlib/LinearAlgebra/Span.lean index aadd53e2e77b1..96db394634db5 100644 --- a/Mathlib/LinearAlgebra/Span.lean +++ b/Mathlib/LinearAlgebra/Span.lean @@ -913,8 +913,8 @@ section DivisionRing variable [DivisionRing K] [AddCommGroup V] [Module K V] -/-- There is no vector subspace between `p` and `(K ∙ x) ⊔ p`, `Wcovby` version. -/ -theorem wcovby_span_singleton_sup (x : V) (p : Submodule K V) : Wcovby p ((K ∙ x) ⊔ p) := by +/-- There is no vector subspace between `p` and `(K ∙ x) ⊔ p`, `WCovBy` version. -/ +theorem wcovBy_span_singleton_sup (x : V) (p : Submodule K V) : WCovBy p ((K ∙ x) ⊔ p) := by refine ⟨le_sup_right, fun q hpq hqp ↦ hqp.not_le ?_⟩ rcases SetLike.exists_of_lt hpq with ⟨y, hyq, hyp⟩ obtain ⟨c, z, hz, rfl⟩ : ∃ c : K, ∃ z ∈ p, c • x + z = y := by @@ -925,9 +925,9 @@ theorem wcovby_span_singleton_sup (x : V) (p : Submodule K V) : Wcovby p ((K ∙ · rwa [q.add_mem_iff_left (hpq.le hz), q.smul_mem_iff hc] at hyq simp [hpq.le, this] -/-- There is no vector subspace between `p` and `(K ∙ x) ⊔ p`, `Covby` version. -/ -theorem covby_span_singleton_sup {x : V} {p : Submodule K V} (h : x ∉ p) : Covby p ((K ∙ x) ⊔ p) := - ⟨by simpa, (wcovby_span_singleton_sup _ _).2⟩ +/-- There is no vector subspace between `p` and `(K ∙ x) ⊔ p`, `CovBy` version. -/ +theorem covBy_span_singleton_sup {x : V} {p : Submodule K V} (h : x ∉ p) : CovBy p ((K ∙ x) ⊔ p) := + ⟨by simpa, (wcovBy_span_singleton_sup _ _).2⟩ end DivisionRing diff --git a/Mathlib/Order/Atoms.lean b/Mathlib/Order/Atoms.lean index da3169717869c..e010975f9e19b 100644 --- a/Mathlib/Order/Atoms.lean +++ b/Mathlib/Order/Atoms.lean @@ -102,13 +102,13 @@ theorem IsAtom.Iic_eq (h : IsAtom a) : Set.Iic a = {⊥, a} := #align is_atom.Iic_eq IsAtom.Iic_eq @[simp] -theorem bot_covby_iff : ⊥ ⋖ a ↔ IsAtom a := by - simp only [Covby, bot_lt_iff_ne_bot, IsAtom, not_imp_not] -#align bot_covby_iff bot_covby_iff +theorem bot_covBy_iff : ⊥ ⋖ a ↔ IsAtom a := by + simp only [CovBy, bot_lt_iff_ne_bot, IsAtom, not_imp_not] +#align bot_covby_iff bot_covBy_iff -alias ⟨Covby.is_atom, IsAtom.bot_covby⟩ := bot_covby_iff -#align covby.is_atom Covby.is_atom -#align is_atom.bot_covby IsAtom.bot_covby +alias ⟨CovBy.is_atom, IsAtom.bot_covBy⟩ := bot_covBy_iff +#align covby.is_atom CovBy.is_atom +#align is_atom.bot_covby IsAtom.bot_covBy end PartialOrder @@ -192,13 +192,13 @@ theorem IsCoatom.Ici_eq (h : IsCoatom a) : Set.Ici a = {⊤, a} := #align is_coatom.Ici_eq IsCoatom.Ici_eq @[simp] -theorem covby_top_iff : a ⋖ ⊤ ↔ IsCoatom a := - toDual_covby_toDual_iff.symm.trans bot_covby_iff -#align covby_top_iff covby_top_iff +theorem covBy_top_iff : a ⋖ ⊤ ↔ IsCoatom a := + toDual_covBy_toDual_iff.symm.trans bot_covBy_iff +#align covby_top_iff covBy_top_iff -alias ⟨Covby.is_coatom, IsCoatom.covby_top⟩ := covby_top_iff -#align covby.is_coatom Covby.is_coatom -#align is_coatom.covby_top IsCoatom.covby_top +alias ⟨CovBy.isCoatom, IsCoatom.covBy_top⟩ := covBy_top_iff +#align covby.is_coatom CovBy.isCoatom +#align is_coatom.covby_top IsCoatom.covBy_top end PartialOrder @@ -214,23 +214,23 @@ variable [PartialOrder α] {a b : α} @[simp] theorem Set.Ici.isAtom_iff {b : Set.Ici a} : IsAtom b ↔ a ⋖ b := by - rw [← bot_covby_iff] - refine' (Set.OrdConnected.apply_covby_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) _).symm + rw [← bot_covBy_iff] + refine' (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) _).symm simpa only [OrderEmbedding.subtype_apply, Subtype.range_coe_subtype] using Set.ordConnected_Ici #align set.Ici.is_atom_iff Set.Ici.isAtom_iff @[simp] theorem Set.Iic.isCoatom_iff {a : Set.Iic b} : IsCoatom a ↔ ↑a ⋖ b := by - rw [← covby_top_iff] - refine' (Set.OrdConnected.apply_covby_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) _).symm + rw [← covBy_top_iff] + refine' (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) _).symm simpa only [OrderEmbedding.subtype_apply, Subtype.range_coe_subtype] using Set.ordConnected_Iic #align set.Iic.is_coatom_iff Set.Iic.isCoatom_iff -theorem covby_iff_atom_Ici (h : a ≤ b) : a ⋖ b ↔ IsAtom (⟨b, h⟩ : Set.Ici a) := by simp -#align covby_iff_atom_Ici covby_iff_atom_Ici +theorem covBy_iff_atom_Ici (h : a ≤ b) : a ⋖ b ↔ IsAtom (⟨b, h⟩ : Set.Ici a) := by simp +#align covby_iff_atom_Ici covBy_iff_atom_Ici -theorem covby_iff_coatom_Iic (h : a ≤ b) : a ⋖ b ↔ IsCoatom (⟨a, h⟩ : Set.Iic b) := by simp -#align covby_iff_coatom_Iic covby_iff_coatom_Iic +theorem covBy_iff_coatom_Iic (h : a ≤ b) : a ⋖ b ↔ IsCoatom (⟨a, h⟩ : Set.Iic b) := by simp +#align covby_iff_coatom_Iic covBy_iff_coatom_Iic end PartialOrder @@ -583,9 +583,9 @@ theorem isCoatom_bot : IsCoatom (⊥ : α) := isAtom_dual_iff_isCoatom.1 isAtom_top #align is_coatom_bot isCoatom_bot -theorem bot_covby_top : (⊥ : α) ⋖ ⊤ := - isAtom_top.bot_covby -#align bot_covby_top bot_covby_top +theorem bot_covBy_top : (⊥ : α) ⋖ ⊤ := + isAtom_top.bot_covBy +#align bot_covby_top bot_covBy_top end IsSimpleOrder @@ -789,8 +789,8 @@ variable [PartialOrder α] [PartialOrder β] theorem isAtom_of_map_bot_of_image [OrderBot α] [OrderBot β] (f : β ↪o α) (hbot : f ⊥ = ⊥) {b : β} (hb : IsAtom (f b)) : IsAtom b := by - simp only [← bot_covby_iff] at hb ⊢ - exact Covby.of_image f (hbot.symm ▸ hb) + simp only [← bot_covBy_iff] at hb ⊢ + exact CovBy.of_image f (hbot.symm ▸ hb) #align order_embedding.is_atom_of_map_bot_of_image OrderEmbedding.isAtom_of_map_bot_of_image theorem isCoatom_of_map_top_of_image [OrderTop α] [OrderTop β] (f : β ↪o α) (htop : f ⊤ = ⊤) diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean index 6a94bcd858a8b..df86a3c970d41 100644 --- a/Mathlib/Order/Cover.lean +++ b/Mathlib/Order/Cover.lean @@ -33,124 +33,124 @@ section Preorder variable [Preorder α] [Preorder β] {a b c : α} -/-- `Wcovby a b` means that `a = b` or `b` covers `a`. +/-- `WCovBy a b` means that `a = b` or `b` covers `a`. This means that `a ≤ b` and there is no element in between. -/ -def Wcovby (a b : α) : Prop := +def WCovBy (a b : α) : Prop := a ≤ b ∧ ∀ ⦃c⦄, a < c → ¬c < b -#align wcovby Wcovby +#align wcovby WCovBy -/-- Notation for `Wcovby a b`. -/ -infixl:50 " ⩿ " => Wcovby +/-- Notation for `WCovBy a b`. -/ +infixl:50 " ⩿ " => WCovBy -theorem Wcovby.le (h : a ⩿ b) : a ≤ b := +theorem WCovBy.le (h : a ⩿ b) : a ≤ b := h.1 -#align wcovby.le Wcovby.le +#align wcovby.le WCovBy.le -theorem Wcovby.refl (a : α) : a ⩿ a := +theorem WCovBy.refl (a : α) : a ⩿ a := ⟨le_rfl, fun _ hc => hc.not_lt⟩ -#align wcovby.refl Wcovby.refl +#align wcovby.refl WCovBy.refl -@[simp] lemma Wcovby.rfl : a ⩿ a := Wcovby.refl a -#align wcovby.rfl Wcovby.rfl +@[simp] lemma WCovBy.rfl : a ⩿ a := WCovBy.refl a +#align wcovby.rfl WCovBy.rfl -protected theorem Eq.wcovby (h : a = b) : a ⩿ b := - h ▸ Wcovby.rfl -#align eq.wcovby Eq.wcovby +protected theorem Eq.wcovBy (h : a = b) : a ⩿ b := + h ▸ WCovBy.rfl +#align eq.wcovby Eq.wcovBy -theorem wcovby_of_le_of_le (h1 : a ≤ b) (h2 : b ≤ a) : a ⩿ b := +theorem wcovBy_of_le_of_le (h1 : a ≤ b) (h2 : b ≤ a) : a ⩿ b := ⟨h1, fun _ hac hcb => (hac.trans hcb).not_le h2⟩ -#align wcovby_of_le_of_le wcovby_of_le_of_le +#align wcovby_of_le_of_le wcovBy_of_le_of_le -alias LE.le.wcovby_of_le := wcovby_of_le_of_le +alias LE.le.wcovBy_of_le := wcovBy_of_le_of_le -theorem AntisymmRel.wcovby (h : AntisymmRel (· ≤ ·) a b) : a ⩿ b := - wcovby_of_le_of_le h.1 h.2 -#align antisymm_rel.wcovby AntisymmRel.wcovby +theorem AntisymmRel.wcovBy (h : AntisymmRel (· ≤ ·) a b) : a ⩿ b := + wcovBy_of_le_of_le h.1 h.2 +#align antisymm_rel.wcovby AntisymmRel.wcovBy -theorem Wcovby.wcovby_iff_le (hab : a ⩿ b) : b ⩿ a ↔ b ≤ a := - ⟨fun h => h.le, fun h => h.wcovby_of_le hab.le⟩ -#align wcovby.wcovby_iff_le Wcovby.wcovby_iff_le +theorem WCovBy.wcovBy_iff_le (hab : a ⩿ b) : b ⩿ a ↔ b ≤ a := + ⟨fun h => h.le, fun h => h.wcovBy_of_le hab.le⟩ +#align wcovby.wcovby_iff_le WCovBy.wcovBy_iff_le -theorem wcovby_of_eq_or_eq (hab : a ≤ b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⩿ b := +theorem wcovBy_of_eq_or_eq (hab : a ≤ b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⩿ b := ⟨hab, fun c ha hb => (h c ha.le hb.le).elim ha.ne' hb.ne⟩ -#align wcovby_of_eq_or_eq wcovby_of_eq_or_eq +#align wcovby_of_eq_or_eq wcovBy_of_eq_or_eq -theorem AntisymmRel.trans_wcovby (hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⩿ c) : a ⩿ c := +theorem AntisymmRel.trans_wcovBy (hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⩿ c) : a ⩿ c := ⟨hab.1.trans hbc.le, fun _ had hdc => hbc.2 (hab.2.trans_lt had) hdc⟩ -#align antisymm_rel.trans_wcovby AntisymmRel.trans_wcovby +#align antisymm_rel.trans_wcovby AntisymmRel.trans_wcovBy -theorem wcovby_congr_left (hab : AntisymmRel (· ≤ ·) a b) : a ⩿ c ↔ b ⩿ c := - ⟨hab.symm.trans_wcovby, hab.trans_wcovby⟩ -#align wcovby_congr_left wcovby_congr_left +theorem wcovBy_congr_left (hab : AntisymmRel (· ≤ ·) a b) : a ⩿ c ↔ b ⩿ c := + ⟨hab.symm.trans_wcovBy, hab.trans_wcovBy⟩ +#align wcovby_congr_left wcovBy_congr_left -theorem Wcovby.trans_antisymm_rel (hab : a ⩿ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⩿ c := +theorem WCovBy.trans_antisymm_rel (hab : a ⩿ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⩿ c := ⟨hab.le.trans hbc.1, fun _ had hdc => hab.2 had <| hdc.trans_le hbc.2⟩ -#align wcovby.trans_antisymm_rel Wcovby.trans_antisymm_rel +#align wcovby.trans_antisymm_rel WCovBy.trans_antisymm_rel -theorem wcovby_congr_right (hab : AntisymmRel (· ≤ ·) a b) : c ⩿ a ↔ c ⩿ b := +theorem wcovBy_congr_right (hab : AntisymmRel (· ≤ ·) a b) : c ⩿ a ↔ c ⩿ b := ⟨fun h => h.trans_antisymm_rel hab, fun h => h.trans_antisymm_rel hab.symm⟩ -#align wcovby_congr_right wcovby_congr_right +#align wcovby_congr_right wcovBy_congr_right /-- If `a ≤ b`, then `b` does not cover `a` iff there's an element in between. -/ -theorem not_wcovby_iff (h : a ≤ b) : ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b := by - simp_rw [Wcovby, h, true_and_iff, not_forall, exists_prop, not_not] -#align not_wcovby_iff not_wcovby_iff +theorem not_wcovBy_iff (h : a ≤ b) : ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b := by + simp_rw [WCovBy, h, true_and_iff, not_forall, exists_prop, not_not] +#align not_wcovby_iff not_wcovBy_iff -instance Wcovby.isRefl : IsRefl α (· ⩿ ·) := - ⟨Wcovby.refl⟩ -#align wcovby.is_refl Wcovby.isRefl +instance WCovBy.isRefl : IsRefl α (· ⩿ ·) := + ⟨WCovBy.refl⟩ +#align wcovby.is_refl WCovBy.isRefl -theorem Wcovby.Ioo_eq (h : a ⩿ b) : Ioo a b = ∅ := +theorem WCovBy.Ioo_eq (h : a ⩿ b) : Ioo a b = ∅ := eq_empty_iff_forall_not_mem.2 fun _ hx => h.2 hx.1 hx.2 -#align wcovby.Ioo_eq Wcovby.Ioo_eq +#align wcovby.Ioo_eq WCovBy.Ioo_eq -theorem wcovby_iff_Ioo_eq : a ⩿ b ↔ a ≤ b ∧ Ioo a b = ∅ := +theorem wcovBy_iff_Ioo_eq : a ⩿ b ↔ a ≤ b ∧ Ioo a b = ∅ := and_congr_right' <| by simp [eq_empty_iff_forall_not_mem] -#align wcovby_iff_Ioo_eq wcovby_iff_Ioo_eq +#align wcovby_iff_Ioo_eq wcovBy_iff_Ioo_eq -lemma Wcovby.of_le_of_le (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : b ⩿ c := +lemma WCovBy.of_le_of_le (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : b ⩿ c := ⟨hbc, fun _x hbx hxc ↦ hac.2 (hab.trans_lt hbx) hxc⟩ -lemma Wcovby.of_le_of_le' (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : a ⩿ b := +lemma WCovBy.of_le_of_le' (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : a ⩿ b := ⟨hab, fun _x hax hxb ↦ hac.2 hax <| hxb.trans_le hbc⟩ -theorem Wcovby.of_image (f : α ↪o β) (h : f a ⩿ f b) : a ⩿ b := +theorem WCovBy.of_image (f : α ↪o β) (h : f a ⩿ f b) : a ⩿ b := ⟨f.le_iff_le.mp h.le, fun _ hac hcb => h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩ -#align wcovby.of_image Wcovby.of_image +#align wcovby.of_image WCovBy.of_image -theorem Wcovby.image (f : α ↪o β) (hab : a ⩿ b) (h : (range f).OrdConnected) : f a ⩿ f b := by +theorem WCovBy.image (f : α ↪o β) (hab : a ⩿ b) (h : (range f).OrdConnected) : f a ⩿ f b := by refine' ⟨f.monotone hab.le, fun c ha hb => _⟩ obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩ rw [f.lt_iff_lt] at ha hb exact hab.2 ha hb -#align wcovby.image Wcovby.image +#align wcovby.image WCovBy.image -theorem Set.OrdConnected.apply_wcovby_apply_iff (f : α ↪o β) (h : (range f).OrdConnected) : +theorem Set.OrdConnected.apply_wcovBy_apply_iff (f : α ↪o β) (h : (range f).OrdConnected) : f a ⩿ f b ↔ a ⩿ b := ⟨fun h2 => h2.of_image f, fun hab => hab.image f h⟩ -#align set.ord_connected.apply_wcovby_apply_iff Set.OrdConnected.apply_wcovby_apply_iff +#align set.ord_connected.apply_wcovby_apply_iff Set.OrdConnected.apply_wcovBy_apply_iff @[simp] -theorem apply_wcovby_apply_iff {E : Type*} [OrderIsoClass E α β] (e : E) : e a ⩿ e b ↔ a ⩿ b := - (ordConnected_range (e : α ≃o β)).apply_wcovby_apply_iff ((e : α ≃o β) : α ↪o β) -#align apply_wcovby_apply_iff apply_wcovby_apply_iff +theorem apply_wcovBy_apply_iff {E : Type*} [OrderIsoClass E α β] (e : E) : e a ⩿ e b ↔ a ⩿ b := + (ordConnected_range (e : α ≃o β)).apply_wcovBy_apply_iff ((e : α ≃o β) : α ↪o β) +#align apply_wcovby_apply_iff apply_wcovBy_apply_iff @[simp] -theorem toDual_wcovby_toDual_iff : toDual b ⩿ toDual a ↔ a ⩿ b := +theorem toDual_wcovBy_toDual_iff : toDual b ⩿ toDual a ↔ a ⩿ b := and_congr_right' <| forall_congr' fun _ => forall_swap -#align to_dual_wcovby_to_dual_iff toDual_wcovby_toDual_iff +#align to_dual_wcovby_to_dual_iff toDual_wcovBy_toDual_iff @[simp] -theorem ofDual_wcovby_ofDual_iff {a b : αᵒᵈ} : ofDual a ⩿ ofDual b ↔ b ⩿ a := +theorem ofDual_wcovBy_ofDual_iff {a b : αᵒᵈ} : ofDual a ⩿ ofDual b ↔ b ⩿ a := and_congr_right' <| forall_congr' fun _ => forall_swap -#align of_dual_wcovby_of_dual_iff ofDual_wcovby_ofDual_iff +#align of_dual_wcovby_of_dual_iff ofDual_wcovBy_ofDual_iff -alias ⟨_, Wcovby.toDual⟩ := toDual_wcovby_toDual_iff -#align wcovby.to_dual Wcovby.toDual +alias ⟨_, WCovBy.toDual⟩ := toDual_wcovBy_toDual_iff +#align wcovby.to_dual WCovBy.toDual -alias ⟨_, Wcovby.ofDual⟩ := ofDual_wcovby_ofDual_iff -#align wcovby.of_dual Wcovby.ofDual +alias ⟨_, WCovBy.ofDual⟩ := ofDual_wcovBy_ofDual_iff +#align wcovby.of_dual WCovBy.ofDual end Preorder @@ -158,34 +158,34 @@ section PartialOrder variable [PartialOrder α] {a b c : α} -theorem Wcovby.eq_or_eq (h : a ⩿ b) (h2 : a ≤ c) (h3 : c ≤ b) : c = a ∨ c = b := by +theorem WCovBy.eq_or_eq (h : a ⩿ b) (h2 : a ≤ c) (h3 : c ≤ b) : c = a ∨ c = b := by rcases h2.eq_or_lt with (h2 | h2); · exact Or.inl h2.symm rcases h3.eq_or_lt with (h3 | h3); · exact Or.inr h3 exact (h.2 h2 h3).elim -#align wcovby.eq_or_eq Wcovby.eq_or_eq +#align wcovby.eq_or_eq WCovBy.eq_or_eq -/-- An `iff` version of `Wcovby.eq_or_eq` and `wcovby_of_eq_or_eq`. -/ -theorem wcovby_iff_le_and_eq_or_eq : a ⩿ b ↔ a ≤ b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b := - ⟨fun h => ⟨h.le, fun _ => h.eq_or_eq⟩, And.rec wcovby_of_eq_or_eq⟩ -#align wcovby_iff_le_and_eq_or_eq wcovby_iff_le_and_eq_or_eq +/-- An `iff` version of `WCovBy.eq_or_eq` and `wcovBy_of_eq_or_eq`. -/ +theorem wcovBy_iff_le_and_eq_or_eq : a ⩿ b ↔ a ≤ b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b := + ⟨fun h => ⟨h.le, fun _ => h.eq_or_eq⟩, And.rec wcovBy_of_eq_or_eq⟩ +#align wcovby_iff_le_and_eq_or_eq wcovBy_iff_le_and_eq_or_eq -theorem Wcovby.le_and_le_iff (h : a ⩿ b) : a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b := by +theorem WCovBy.le_and_le_iff (h : a ⩿ b) : a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b := by refine' ⟨fun h2 => h.eq_or_eq h2.1 h2.2, _⟩; rintro (rfl | rfl); exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩] -#align wcovby.le_and_le_iff Wcovby.le_and_le_iff +#align wcovby.le_and_le_iff WCovBy.le_and_le_iff -theorem Wcovby.Icc_eq (h : a ⩿ b) : Icc a b = {a, b} := by +theorem WCovBy.Icc_eq (h : a ⩿ b) : Icc a b = {a, b} := by ext c exact h.le_and_le_iff -#align wcovby.Icc_eq Wcovby.Icc_eq +#align wcovby.Icc_eq WCovBy.Icc_eq -theorem Wcovby.Ico_subset (h : a ⩿ b) : Ico a b ⊆ {a} := by +theorem WCovBy.Ico_subset (h : a ⩿ b) : Ico a b ⊆ {a} := by rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm] -#align wcovby.Ico_subset Wcovby.Ico_subset +#align wcovby.Ico_subset WCovBy.Ico_subset -theorem Wcovby.Ioc_subset (h : a ⩿ b) : Ioc a b ⊆ {b} := by +theorem WCovBy.Ioc_subset (h : a ⩿ b) : Ioc a b ⊆ {b} := by rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff] -#align wcovby.Ioc_subset Wcovby.Ioc_subset +#align wcovby.Ioc_subset WCovBy.Ioc_subset end PartialOrder @@ -193,10 +193,10 @@ section SemilatticeSup variable [SemilatticeSup α] {a b c : α} -theorem Wcovby.sup_eq (hac : a ⩿ c) (hbc : b ⩿ c) (hab : a ≠ b) : a ⊔ b = c := +theorem WCovBy.sup_eq (hac : a ⩿ c) (hbc : b ⩿ c) (hab : a ≠ b) : a ⊔ b = c := (sup_le hac.le hbc.le).eq_of_not_lt fun h => hab.lt_sup_or_lt_sup.elim (fun h' => hac.2 h' h) fun h' => hbc.2 h' h -#align wcovby.sup_eq Wcovby.sup_eq +#align wcovby.sup_eq WCovBy.sup_eq end SemilatticeSup @@ -204,9 +204,9 @@ section SemilatticeInf variable [SemilatticeInf α] {a b c : α} -theorem Wcovby.inf_eq (hca : c ⩿ a) (hcb : c ⩿ b) (hab : a ≠ b) : a ⊓ b = c := +theorem WCovBy.inf_eq (hca : c ⩿ a) (hcb : c ⩿ b) (hab : a ≠ b) : a ⊓ b = c := (le_inf hca.le hcb.le).eq_of_not_gt fun h => hab.inf_lt_or_inf_lt.elim (hca.2 h) (hcb.2 h) -#align wcovby.inf_eq Wcovby.inf_eq +#align wcovby.inf_eq WCovBy.inf_eq end SemilatticeInf @@ -216,54 +216,54 @@ section LT variable [LT α] {a b : α} -/-- `Covby a b` means that `b` covers `a`: `a < b` and there is no element in between. -/ -def Covby (a b : α) : Prop := +/-- `CovBy a b` means that `b` covers `a`: `a < b` and there is no element in between. -/ +def CovBy (a b : α) : Prop := a < b ∧ ∀ ⦃c⦄, a < c → ¬c < b -#align covby Covby +#align covby CovBy -/-- Notation for `Covby a b`. -/ -infixl:50 " ⋖ " => Covby +/-- Notation for `CovBy a b`. -/ +infixl:50 " ⋖ " => CovBy -theorem Covby.lt (h : a ⋖ b) : a < b := +theorem CovBy.lt (h : a ⋖ b) : a < b := h.1 -#align covby.lt Covby.lt +#align covby.lt CovBy.lt /-- If `a < b`, then `b` does not cover `a` iff there's an element in between. -/ -theorem not_covby_iff (h : a < b) : ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b := by - simp_rw [Covby, h, true_and_iff, not_forall, exists_prop, not_not] -#align not_covby_iff not_covby_iff +theorem not_covBy_iff (h : a < b) : ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b := by + simp_rw [CovBy, h, true_and_iff, not_forall, exists_prop, not_not] +#align not_covby_iff not_covBy_iff -alias ⟨exists_lt_lt_of_not_covby, _⟩ := not_covby_iff -#align exists_lt_lt_of_not_covby exists_lt_lt_of_not_covby +alias ⟨exists_lt_lt_of_not_covBy, _⟩ := not_covBy_iff +#align exists_lt_lt_of_not_covby exists_lt_lt_of_not_covBy -alias LT.lt.exists_lt_lt := exists_lt_lt_of_not_covby +alias LT.lt.exists_lt_lt := exists_lt_lt_of_not_covBy /-- In a dense order, nothing covers anything. -/ -theorem not_covby [DenselyOrdered α] : ¬a ⋖ b := fun h => +theorem not_covBy [DenselyOrdered α] : ¬a ⋖ b := fun h => let ⟨_, hc⟩ := exists_between h.1 h.2 hc.1 hc.2 -#align not_covby not_covby +#align not_covby not_covBy -theorem densely_ordered_iff_forall_not_covby : DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b := - ⟨fun h _ _ => @not_covby _ _ _ _ h, fun h => - ⟨fun _ _ hab => exists_lt_lt_of_not_covby hab <| h _ _⟩⟩ -#align densely_ordered_iff_forall_not_covby densely_ordered_iff_forall_not_covby +theorem densely_ordered_iff_forall_not_covBy : DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b := + ⟨fun h _ _ => @not_covBy _ _ _ _ h, fun h => + ⟨fun _ _ hab => exists_lt_lt_of_not_covBy hab <| h _ _⟩⟩ +#align densely_ordered_iff_forall_not_covby densely_ordered_iff_forall_not_covBy @[simp] -theorem toDual_covby_toDual_iff : toDual b ⋖ toDual a ↔ a ⋖ b := +theorem toDual_covBy_toDual_iff : toDual b ⋖ toDual a ↔ a ⋖ b := and_congr_right' <| forall_congr' fun _ => forall_swap -#align to_dual_covby_to_dual_iff toDual_covby_toDual_iff +#align to_dual_covby_to_dual_iff toDual_covBy_toDual_iff @[simp] -theorem ofDual_covby_ofDual_iff {a b : αᵒᵈ} : ofDual a ⋖ ofDual b ↔ b ⋖ a := +theorem ofDual_covBy_ofDual_iff {a b : αᵒᵈ} : ofDual a ⋖ ofDual b ↔ b ⋖ a := and_congr_right' <| forall_congr' fun _ => forall_swap -#align of_dual_covby_of_dual_iff ofDual_covby_ofDual_iff +#align of_dual_covby_of_dual_iff ofDual_covBy_ofDual_iff -alias ⟨_, Covby.toDual⟩ := toDual_covby_toDual_iff -#align covby.to_dual Covby.toDual +alias ⟨_, CovBy.toDual⟩ := toDual_covBy_toDual_iff +#align covby.to_dual CovBy.toDual -alias ⟨_, Covby.ofDual⟩ := ofDual_covby_ofDual_iff -#align covby.of_dual Covby.ofDual +alias ⟨_, CovBy.ofDual⟩ := ofDual_covBy_ofDual_iff +#align covby.of_dual CovBy.ofDual end LT @@ -271,106 +271,106 @@ section Preorder variable [Preorder α] [Preorder β] {a b c : α} -theorem Covby.le (h : a ⋖ b) : a ≤ b := +theorem CovBy.le (h : a ⋖ b) : a ≤ b := h.1.le -#align covby.le Covby.le +#align covby.le CovBy.le -protected theorem Covby.ne (h : a ⋖ b) : a ≠ b := +protected theorem CovBy.ne (h : a ⋖ b) : a ≠ b := h.lt.ne -#align covby.ne Covby.ne +#align covby.ne CovBy.ne -theorem Covby.ne' (h : a ⋖ b) : b ≠ a := +theorem CovBy.ne' (h : a ⋖ b) : b ≠ a := h.lt.ne' -#align covby.ne' Covby.ne' +#align covby.ne' CovBy.ne' -protected theorem Covby.wcovby (h : a ⋖ b) : a ⩿ b := +protected theorem CovBy.wcovBy (h : a ⋖ b) : a ⩿ b := ⟨h.le, h.2⟩ -#align covby.wcovby Covby.wcovby +#align covby.wcovby CovBy.wcovBy -theorem Wcovby.covby_of_not_le (h : a ⩿ b) (h2 : ¬b ≤ a) : a ⋖ b := +theorem WCovBy.covBy_of_not_le (h : a ⩿ b) (h2 : ¬b ≤ a) : a ⋖ b := ⟨h.le.lt_of_not_le h2, h.2⟩ -#align wcovby.covby_of_not_le Wcovby.covby_of_not_le +#align wcovby.covby_of_not_le WCovBy.covBy_of_not_le -theorem Wcovby.covby_of_lt (h : a ⩿ b) (h2 : a < b) : a ⋖ b := +theorem WCovBy.covBy_of_lt (h : a ⩿ b) (h2 : a < b) : a ⋖ b := ⟨h2, h.2⟩ -#align wcovby.covby_of_lt Wcovby.covby_of_lt +#align wcovby.covby_of_lt WCovBy.covBy_of_lt -lemma Covby.of_le_of_lt (hac : a ⋖ c) (hab : a ≤ b) (hbc : b < c) : b ⋖ c := +lemma CovBy.of_le_of_lt (hac : a ⋖ c) (hab : a ≤ b) (hbc : b < c) : b ⋖ c := ⟨hbc, fun _x hbx hxc ↦ hac.2 (hab.trans_lt hbx) hxc⟩ -lemma Covby.of_lt_of_le (hac : a ⋖ c) (hab : a < b) (hbc : b ≤ c) : a ⋖ b := +lemma CovBy.of_lt_of_le (hac : a ⋖ c) (hab : a < b) (hbc : b ≤ c) : a ⋖ b := ⟨hab, fun _x hax hxb ↦ hac.2 hax <| hxb.trans_le hbc⟩ -theorem not_covby_of_lt_of_lt (h₁ : a < b) (h₂ : b < c) : ¬a ⋖ c := - (not_covby_iff (h₁.trans h₂)).2 ⟨b, h₁, h₂⟩ -#align not_covby_of_lt_of_lt not_covby_of_lt_of_lt +theorem not_covBy_of_lt_of_lt (h₁ : a < b) (h₂ : b < c) : ¬a ⋖ c := + (not_covBy_iff (h₁.trans h₂)).2 ⟨b, h₁, h₂⟩ +#align not_covby_of_lt_of_lt not_covBy_of_lt_of_lt -theorem covby_iff_wcovby_and_lt : a ⋖ b ↔ a ⩿ b ∧ a < b := - ⟨fun h => ⟨h.wcovby, h.lt⟩, fun h => h.1.covby_of_lt h.2⟩ -#align covby_iff_wcovby_and_lt covby_iff_wcovby_and_lt +theorem covBy_iff_wcovBy_and_lt : a ⋖ b ↔ a ⩿ b ∧ a < b := + ⟨fun h => ⟨h.wcovBy, h.lt⟩, fun h => h.1.covBy_of_lt h.2⟩ +#align covby_iff_wcovby_and_lt covBy_iff_wcovBy_and_lt -theorem covby_iff_wcovby_and_not_le : a ⋖ b ↔ a ⩿ b ∧ ¬b ≤ a := - ⟨fun h => ⟨h.wcovby, h.lt.not_le⟩, fun h => h.1.covby_of_not_le h.2⟩ -#align covby_iff_wcovby_and_not_le covby_iff_wcovby_and_not_le +theorem covBy_iff_wcovBy_and_not_le : a ⋖ b ↔ a ⩿ b ∧ ¬b ≤ a := + ⟨fun h => ⟨h.wcovBy, h.lt.not_le⟩, fun h => h.1.covBy_of_not_le h.2⟩ +#align covby_iff_wcovby_and_not_le covBy_iff_wcovBy_and_not_le -theorem wcovby_iff_covby_or_le_and_le : a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a := - ⟨fun h => or_iff_not_imp_right.mpr fun h' => h.covby_of_not_le fun hba => h' ⟨h.le, hba⟩, - fun h' => h'.elim (fun h => h.wcovby) fun h => h.1.wcovby_of_le h.2⟩ -#align wcovby_iff_covby_or_le_and_le wcovby_iff_covby_or_le_and_le +theorem wcovBy_iff_covBy_or_le_and_le : a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a := + ⟨fun h => or_iff_not_imp_right.mpr fun h' => h.covBy_of_not_le fun hba => h' ⟨h.le, hba⟩, + fun h' => h'.elim (fun h => h.wcovBy) fun h => h.1.wcovBy_of_le h.2⟩ +#align wcovby_iff_covby_or_le_and_le wcovBy_iff_covBy_or_le_and_le -theorem AntisymmRel.trans_covby (hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⋖ c) : a ⋖ c := +theorem AntisymmRel.trans_covBy (hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⋖ c) : a ⋖ c := ⟨hab.1.trans_lt hbc.lt, fun _ had hdc => hbc.2 (hab.2.trans_lt had) hdc⟩ -#align antisymm_rel.trans_covby AntisymmRel.trans_covby +#align antisymm_rel.trans_covby AntisymmRel.trans_covBy -theorem covby_congr_left (hab : AntisymmRel (· ≤ ·) a b) : a ⋖ c ↔ b ⋖ c := - ⟨hab.symm.trans_covby, hab.trans_covby⟩ -#align covby_congr_left covby_congr_left +theorem covBy_congr_left (hab : AntisymmRel (· ≤ ·) a b) : a ⋖ c ↔ b ⋖ c := + ⟨hab.symm.trans_covBy, hab.trans_covBy⟩ +#align covby_congr_left covBy_congr_left -theorem Covby.trans_antisymmRel (hab : a ⋖ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⋖ c := +theorem CovBy.trans_antisymmRel (hab : a ⋖ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⋖ c := ⟨hab.lt.trans_le hbc.1, fun _ had hdb => hab.2 had <| hdb.trans_le hbc.2⟩ -#align covby.trans_antisymm_rel Covby.trans_antisymmRel +#align covby.trans_antisymm_rel CovBy.trans_antisymmRel -theorem covby_congr_right (hab : AntisymmRel (· ≤ ·) a b) : c ⋖ a ↔ c ⋖ b := +theorem covBy_congr_right (hab : AntisymmRel (· ≤ ·) a b) : c ⋖ a ↔ c ⋖ b := ⟨fun h => h.trans_antisymmRel hab, fun h => h.trans_antisymmRel hab.symm⟩ -#align covby_congr_right covby_congr_right +#align covby_congr_right covBy_congr_right instance : IsNonstrictStrictOrder α (· ⩿ ·) (· ⋖ ·) := ⟨fun _ _ => - covby_iff_wcovby_and_not_le.trans <| and_congr_right fun h => h.wcovby_iff_le.not.symm⟩ + covBy_iff_wcovBy_and_not_le.trans <| and_congr_right fun h => h.wcovBy_iff_le.not.symm⟩ -instance Covby.isIrrefl : IsIrrefl α (· ⋖ ·) := +instance CovBy.isIrrefl : IsIrrefl α (· ⋖ ·) := ⟨fun _ ha => ha.ne rfl⟩ -#align covby.is_irrefl Covby.isIrrefl +#align covby.is_irrefl CovBy.isIrrefl -theorem Covby.Ioo_eq (h : a ⋖ b) : Ioo a b = ∅ := - h.wcovby.Ioo_eq -#align covby.Ioo_eq Covby.Ioo_eq +theorem CovBy.Ioo_eq (h : a ⋖ b) : Ioo a b = ∅ := + h.wcovBy.Ioo_eq +#align covby.Ioo_eq CovBy.Ioo_eq -theorem covby_iff_Ioo_eq : a ⋖ b ↔ a < b ∧ Ioo a b = ∅ := +theorem covBy_iff_Ioo_eq : a ⋖ b ↔ a < b ∧ Ioo a b = ∅ := and_congr_right' <| by simp [eq_empty_iff_forall_not_mem] -#align covby_iff_Ioo_eq covby_iff_Ioo_eq +#align covby_iff_Ioo_eq covBy_iff_Ioo_eq -theorem Covby.of_image (f : α ↪o β) (h : f a ⋖ f b) : a ⋖ b := +theorem CovBy.of_image (f : α ↪o β) (h : f a ⋖ f b) : a ⋖ b := ⟨f.lt_iff_lt.mp h.lt, fun _ hac hcb => h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩ -#align covby.of_image Covby.of_image +#align covby.of_image CovBy.of_image -theorem Covby.image (f : α ↪o β) (hab : a ⋖ b) (h : (range f).OrdConnected) : f a ⋖ f b := - (hab.wcovby.image f h).covby_of_lt <| f.strictMono hab.lt -#align covby.image Covby.image +theorem CovBy.image (f : α ↪o β) (hab : a ⋖ b) (h : (range f).OrdConnected) : f a ⋖ f b := + (hab.wcovBy.image f h).covBy_of_lt <| f.strictMono hab.lt +#align covby.image CovBy.image -theorem Set.OrdConnected.apply_covby_apply_iff (f : α ↪o β) (h : (range f).OrdConnected) : +theorem Set.OrdConnected.apply_covBy_apply_iff (f : α ↪o β) (h : (range f).OrdConnected) : f a ⋖ f b ↔ a ⋖ b := - ⟨Covby.of_image f, fun hab => hab.image f h⟩ -#align set.ord_connected.apply_covby_apply_iff Set.OrdConnected.apply_covby_apply_iff + ⟨CovBy.of_image f, fun hab => hab.image f h⟩ +#align set.ord_connected.apply_covby_apply_iff Set.OrdConnected.apply_covBy_apply_iff @[simp] -theorem apply_covby_apply_iff {E : Type*} [OrderIsoClass E α β] (e : E) : e a ⋖ e b ↔ a ⋖ b := - (ordConnected_range (e : α ≃o β)).apply_covby_apply_iff ((e : α ≃o β) : α ↪o β) -#align apply_covby_apply_iff apply_covby_apply_iff +theorem apply_covBy_apply_iff {E : Type*} [OrderIsoClass E α β] (e : E) : e a ⋖ e b ↔ a ⋖ b := + (ordConnected_range (e : α ≃o β)).apply_covBy_apply_iff ((e : α ≃o β) : α ↪o β) +#align apply_covby_apply_iff apply_covBy_apply_iff -theorem covby_of_eq_or_eq (hab : a < b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⋖ b := +theorem covBy_of_eq_or_eq (hab : a < b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⋖ b := ⟨hab, fun c ha hb => (h c ha.le hb.le).elim ha.ne' hb.ne⟩ -#align covby_of_eq_or_eq covby_of_eq_or_eq +#align covby_of_eq_or_eq covBy_of_eq_or_eq end Preorder @@ -378,48 +378,48 @@ section PartialOrder variable [PartialOrder α] {a b c : α} -theorem Wcovby.covby_of_ne (h : a ⩿ b) (h2 : a ≠ b) : a ⋖ b := +theorem WCovBy.covBy_of_ne (h : a ⩿ b) (h2 : a ≠ b) : a ⋖ b := ⟨h.le.lt_of_ne h2, h.2⟩ -#align wcovby.covby_of_ne Wcovby.covby_of_ne +#align wcovby.covby_of_ne WCovBy.covBy_of_ne -theorem covby_iff_wcovby_and_ne : a ⋖ b ↔ a ⩿ b ∧ a ≠ b := - ⟨fun h => ⟨h.wcovby, h.ne⟩, fun h => h.1.covby_of_ne h.2⟩ -#align covby_iff_wcovby_and_ne covby_iff_wcovby_and_ne +theorem covBy_iff_wcovBy_and_ne : a ⋖ b ↔ a ⩿ b ∧ a ≠ b := + ⟨fun h => ⟨h.wcovBy, h.ne⟩, fun h => h.1.covBy_of_ne h.2⟩ +#align covby_iff_wcovby_and_ne covBy_iff_wcovBy_and_ne -theorem wcovby_iff_covby_or_eq : a ⩿ b ↔ a ⋖ b ∨ a = b := by - rw [le_antisymm_iff, wcovby_iff_covby_or_le_and_le] -#align wcovby_iff_covby_or_eq wcovby_iff_covby_or_eq +theorem wcovBy_iff_covBy_or_eq : a ⩿ b ↔ a ⋖ b ∨ a = b := by + rw [le_antisymm_iff, wcovBy_iff_covBy_or_le_and_le] +#align wcovby_iff_covby_or_eq wcovBy_iff_covBy_or_eq -theorem wcovby_iff_eq_or_covby : a ⩿ b ↔ a = b ∨ a ⋖ b := - wcovby_iff_covby_or_eq.trans or_comm -#align wcovby_iff_eq_or_covby wcovby_iff_eq_or_covby +theorem wcovBy_iff_eq_or_covBy : a ⩿ b ↔ a = b ∨ a ⋖ b := + wcovBy_iff_covBy_or_eq.trans or_comm +#align wcovby_iff_eq_or_covby wcovBy_iff_eq_or_covBy -alias ⟨Wcovby.covby_or_eq, _⟩ := wcovby_iff_covby_or_eq -#align wcovby.covby_or_eq Wcovby.covby_or_eq +alias ⟨WCovBy.covBy_or_eq, _⟩ := wcovBy_iff_covBy_or_eq +#align wcovby.covby_or_eq WCovBy.covBy_or_eq -alias ⟨Wcovby.eq_or_covby, _⟩ := wcovby_iff_eq_or_covby -#align wcovby.eq_or_covby Wcovby.eq_or_covby +alias ⟨WCovBy.eq_or_covBy, _⟩ := wcovBy_iff_eq_or_covBy +#align wcovby.eq_or_covby WCovBy.eq_or_covBy -theorem Covby.eq_or_eq (h : a ⋖ b) (h2 : a ≤ c) (h3 : c ≤ b) : c = a ∨ c = b := - h.wcovby.eq_or_eq h2 h3 -#align covby.eq_or_eq Covby.eq_or_eq +theorem CovBy.eq_or_eq (h : a ⋖ b) (h2 : a ≤ c) (h3 : c ≤ b) : c = a ∨ c = b := + h.wcovBy.eq_or_eq h2 h3 +#align covby.eq_or_eq CovBy.eq_or_eq -/-- An `iff` version of `Covby.eq_or_eq` and `covby_of_eq_or_eq`. -/ -theorem covby_iff_lt_and_eq_or_eq : a ⋖ b ↔ a < b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b := - ⟨fun h => ⟨h.lt, fun _ => h.eq_or_eq⟩, And.rec covby_of_eq_or_eq⟩ -#align covby_iff_lt_and_eq_or_eq covby_iff_lt_and_eq_or_eq +/-- An `iff` version of `CovBy.eq_or_eq` and `covBy_of_eq_or_eq`. -/ +theorem covBy_iff_lt_and_eq_or_eq : a ⋖ b ↔ a < b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b := + ⟨fun h => ⟨h.lt, fun _ => h.eq_or_eq⟩, And.rec covBy_of_eq_or_eq⟩ +#align covby_iff_lt_and_eq_or_eq covBy_iff_lt_and_eq_or_eq -theorem Covby.Ico_eq (h : a ⋖ b) : Ico a b = {a} := by +theorem CovBy.Ico_eq (h : a ⋖ b) : Ico a b = {a} := by rw [← Ioo_union_left h.lt, h.Ioo_eq, empty_union] -#align covby.Ico_eq Covby.Ico_eq +#align covby.Ico_eq CovBy.Ico_eq -theorem Covby.Ioc_eq (h : a ⋖ b) : Ioc a b = {b} := by +theorem CovBy.Ioc_eq (h : a ⋖ b) : Ioc a b = {b} := by rw [← Ioo_union_right h.lt, h.Ioo_eq, empty_union] -#align covby.Ioc_eq Covby.Ioc_eq +#align covby.Ioc_eq CovBy.Ioc_eq -theorem Covby.Icc_eq (h : a ⋖ b) : Icc a b = {a, b} := - h.wcovby.Icc_eq -#align covby.Icc_eq Covby.Icc_eq +theorem CovBy.Icc_eq (h : a ⋖ b) : Icc a b = {a, b} := + h.wcovBy.Icc_eq +#align covby.Icc_eq CovBy.Icc_eq end PartialOrder @@ -427,43 +427,43 @@ section LinearOrder variable [LinearOrder α] {a b c : α} -theorem Covby.Ioi_eq (h : a ⋖ b) : Ioi a = Ici b := by +theorem CovBy.Ioi_eq (h : a ⋖ b) : Ioi a = Ici b := by rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union] -#align covby.Ioi_eq Covby.Ioi_eq +#align covby.Ioi_eq CovBy.Ioi_eq -theorem Covby.Iio_eq (h : a ⋖ b) : Iio b = Iic a := by +theorem CovBy.Iio_eq (h : a ⋖ b) : Iio b = Iic a := by rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty] -#align covby.Iio_eq Covby.Iio_eq +#align covby.Iio_eq CovBy.Iio_eq -theorem Wcovby.le_of_lt (hab : a ⩿ b) (hcb : c < b) : c ≤ a := +theorem WCovBy.le_of_lt (hab : a ⩿ b) (hcb : c < b) : c ≤ a := not_lt.1 fun hac => hab.2 hac hcb -#align wcovby.le_of_lt Wcovby.le_of_lt +#align wcovby.le_of_lt WCovBy.le_of_lt -theorem Wcovby.ge_of_gt (hab : a ⩿ b) (hac : a < c) : b ≤ c := +theorem WCovBy.ge_of_gt (hab : a ⩿ b) (hac : a < c) : b ≤ c := not_lt.1 <| hab.2 hac -#align wcovby.ge_of_gt Wcovby.ge_of_gt +#align wcovby.ge_of_gt WCovBy.ge_of_gt -theorem Covby.le_of_lt (hab : a ⋖ b) : c < b → c ≤ a := - hab.wcovby.le_of_lt -#align covby.le_of_lt Covby.le_of_lt +theorem CovBy.le_of_lt (hab : a ⋖ b) : c < b → c ≤ a := + hab.wcovBy.le_of_lt +#align covby.le_of_lt CovBy.le_of_lt -theorem Covby.ge_of_gt (hab : a ⋖ b) : a < c → b ≤ c := - hab.wcovby.ge_of_gt -#align covby.ge_of_gt Covby.ge_of_gt +theorem CovBy.ge_of_gt (hab : a ⋖ b) : a < c → b ≤ c := + hab.wcovBy.ge_of_gt +#align covby.ge_of_gt CovBy.ge_of_gt -theorem Covby.unique_left (ha : a ⋖ c) (hb : b ⋖ c) : a = b := +theorem CovBy.unique_left (ha : a ⋖ c) (hb : b ⋖ c) : a = b := (hb.le_of_lt ha.lt).antisymm <| ha.le_of_lt hb.lt -#align covby.unique_left Covby.unique_left +#align covby.unique_left CovBy.unique_left -theorem Covby.unique_right (hb : a ⋖ b) (hc : a ⋖ c) : b = c := +theorem CovBy.unique_right (hb : a ⋖ b) (hc : a ⋖ c) : b = c := (hb.ge_of_gt hc.lt).antisymm <| hc.ge_of_gt hb.lt -#align covby.unique_right Covby.unique_right +#align covby.unique_right CovBy.unique_right /-- If `a`, `b`, `c` are consecutive and `a < x < c` then `x = b`. -/ -theorem Covby.eq_of_between {x : α} (hab : a ⋖ b) (hbc : b ⋖ c) (hax : a < x) (hxc : x < c) : +theorem CovBy.eq_of_between {x : α} (hab : a ⋖ b) (hbc : b ⋖ c) (hax : a < x) (hxc : x < c) : x = b := le_antisymm (le_of_not_lt fun h => hbc.2 h hxc) (le_of_not_lt <| hab.2 hax) -#align covby.eq_of_between Covby.eq_of_between +#align covby.eq_of_between CovBy.eq_of_between /-- If `a < b` then there exist `a' > a` and `b' < b` such that `Set.Iio a'` is strictly to the left of `Set.Ioi b'`. -/ @@ -479,42 +479,42 @@ end LinearOrder namespace Set variable {s t : Set α} {a : α} -@[simp] lemma wcovby_insert (x : α) (s : Set α) : s ⩿ insert x s := by - refine' wcovby_of_eq_or_eq (subset_insert x s) fun t hst h2t => _ +@[simp] lemma wcovBy_insert (x : α) (s : Set α) : s ⩿ insert x s := by + refine' wcovBy_of_eq_or_eq (subset_insert x s) fun t hst h2t => _ by_cases h : x ∈ t · exact Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩) · refine' Or.inl (subset_antisymm _ hst) rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff] -#align set.wcovby_insert Set.wcovby_insert +#align set.wcovby_insert Set.wcovBy_insert -@[simp] lemma sdiff_singleton_wcovby (s : Set α) (a : α) : s \ {a} ⩿ s := by +@[simp] lemma sdiff_singleton_wcovBy (s : Set α) (a : α) : s \ {a} ⩿ s := by by_cases ha : a ∈ s - · convert wcovby_insert a _ + · convert wcovBy_insert a _ ext simp [ha] · simp [ha] -@[simp] lemma covby_insert (ha : a ∉ s) : s ⋖ insert a s := - (wcovby_insert _ _).covby_of_lt <| ssubset_insert ha -#align set.covby_insert Set.covby_insert +@[simp] lemma covBy_insert (ha : a ∉ s) : s ⋖ insert a s := + (wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha +#align set.covby_insert Set.covBy_insert -@[simp] lemma sdiff_singleton_covby (ha : a ∈ s) : s \ {a} ⋖ s := - ⟨sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _, (sdiff_singleton_wcovby _ _).2⟩ +@[simp] lemma sdiff_singleton_covBy (ha : a ∈ s) : s \ {a} ⋖ s := + ⟨sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _, (sdiff_singleton_wcovBy _ _).2⟩ -lemma _root_.Covby.exists_set_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t := +lemma _root_.CovBy.exists_set_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t := let ⟨a, ha, hst⟩ := ssubset_iff_insert.1 h.lt ⟨a, ha, (hst.eq_of_not_ssuperset <| h.2 <| ssubset_insert ha).symm⟩ -lemma _root_.Covby.exists_set_sdiff_singleton (h : s ⋖ t) : ∃ a ∈ t, t \ {a} = s := +lemma _root_.CovBy.exists_set_sdiff_singleton (h : s ⋖ t) : ∃ a ∈ t, t \ {a} = s := let ⟨a, ha, hst⟩ := ssubset_iff_sdiff_singleton.1 h.lt ⟨a, ha, (hst.eq_of_not_ssubset fun h' ↦ h.2 h' <| sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _).symm⟩ -lemma covby_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t := - ⟨Covby.exists_set_insert, by rintro ⟨a, ha, rfl⟩; exact covby_insert ha⟩ +lemma covBy_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t := + ⟨CovBy.exists_set_insert, by rintro ⟨a, ha, rfl⟩; exact covBy_insert ha⟩ -lemma covby_iff_exists_sdiff_singleton : s ⋖ t ↔ ∃ a ∈ t, t \ {a} = s := - ⟨Covby.exists_set_sdiff_singleton, by rintro ⟨a, ha, rfl⟩; exact sdiff_singleton_covby ha⟩ +lemma covBy_iff_exists_sdiff_singleton : s ⋖ t ↔ ∃ a ∈ t, t \ {a} = s := + ⟨CovBy.exists_set_sdiff_singleton, by rintro ⟨a, ha, rfl⟩; exact sdiff_singleton_covBy ha⟩ end Set @@ -522,16 +522,16 @@ section Relation open Relation -lemma wcovby_eq_reflGen_covby [PartialOrder α] : ((· : α) ⩿ ·) = ReflGen (· ⋖ ·) := by - ext x y; simp_rw [wcovby_iff_eq_or_covby, @eq_comm _ x, reflGen_iff] +lemma wcovBy_eq_reflGen_covBy [PartialOrder α] : ((· : α) ⩿ ·) = ReflGen (· ⋖ ·) := by + ext x y; simp_rw [wcovBy_iff_eq_or_covBy, @eq_comm _ x, reflGen_iff] -lemma transGen_wcovby_eq_reflTransGen_covby [PartialOrder α] : +lemma transGen_wcovBy_eq_reflTransGen_covBy [PartialOrder α] : TransGen ((· : α) ⩿ ·) = ReflTransGen (· ⋖ ·) := by - rw [wcovby_eq_reflGen_covby, transGen_reflGen] + rw [wcovBy_eq_reflGen_covBy, transGen_reflGen] -lemma reflTransGen_wcovby_eq_reflTransGen_covby [PartialOrder α] : +lemma reflTransGen_wcovBy_eq_reflTransGen_covBy [PartialOrder α] : ReflTransGen ((· : α) ⩿ ·) = ReflTransGen (· ⋖ ·) := by - rw [wcovby_eq_reflGen_covby, reflTransGen_reflGen] + rw [wcovBy_eq_reflGen_covBy, reflTransGen_reflGen] end Relation @@ -540,80 +540,80 @@ namespace Prod variable [PartialOrder α] [PartialOrder β] {a a₁ a₂ : α} {b b₁ b₂ : β} {x y : α × β} @[simp] -theorem swap_wcovby_swap : x.swap ⩿ y.swap ↔ x ⩿ y := - apply_wcovby_apply_iff (OrderIso.prodComm : α × β ≃o β × α) -#align prod.swap_wcovby_swap Prod.swap_wcovby_swap +theorem swap_wcovBy_swap : x.swap ⩿ y.swap ↔ x ⩿ y := + apply_wcovBy_apply_iff (OrderIso.prodComm : α × β ≃o β × α) +#align prod.swap_wcovby_swap Prod.swap_wcovBy_swap @[simp] -theorem swap_covby_swap : x.swap ⋖ y.swap ↔ x ⋖ y := - apply_covby_apply_iff (OrderIso.prodComm : α × β ≃o β × α) -#align prod.swap_covby_swap Prod.swap_covby_swap +theorem swap_covBy_swap : x.swap ⋖ y.swap ↔ x ⋖ y := + apply_covBy_apply_iff (OrderIso.prodComm : α × β ≃o β × α) +#align prod.swap_covby_swap Prod.swap_covBy_swap -theorem fst_eq_or_snd_eq_of_wcovby : x ⩿ y → x.1 = y.1 ∨ x.2 = y.2 := by +theorem fst_eq_or_snd_eq_of_wcovBy : x ⩿ y → x.1 = y.1 ∨ x.2 = y.2 := by refine' fun h => of_not_not fun hab => _ push_neg at hab exact h.2 (mk_lt_mk.2 <| Or.inl ⟨hab.1.lt_of_le h.1.1, le_rfl⟩) (mk_lt_mk.2 <| Or.inr ⟨le_rfl, hab.2.lt_of_le h.1.2⟩) -#align prod.fst_eq_or_snd_eq_of_wcovby Prod.fst_eq_or_snd_eq_of_wcovby +#align prod.fst_eq_or_snd_eq_of_wcovby Prod.fst_eq_or_snd_eq_of_wcovBy -theorem _root_.Wcovby.fst (h : x ⩿ y) : x.1 ⩿ y.1 := +theorem _root_.WCovBy.fst (h : x ⩿ y) : x.1 ⩿ y.1 := ⟨h.1.1, fun _ h₁ h₂ => h.2 (mk_lt_mk_iff_left.2 h₁) ⟨⟨h₂.le, h.1.2⟩, fun hc => h₂.not_le hc.1⟩⟩ -#align wcovby.fst Wcovby.fst +#align wcovby.fst WCovBy.fst -theorem _root_.Wcovby.snd (h : x ⩿ y) : x.2 ⩿ y.2 := +theorem _root_.WCovBy.snd (h : x ⩿ y) : x.2 ⩿ y.2 := ⟨h.1.2, fun _ h₁ h₂ => h.2 (mk_lt_mk_iff_right.2 h₁) ⟨⟨h.1.1, h₂.le⟩, fun hc => h₂.not_le hc.2⟩⟩ -#align wcovby.snd Wcovby.snd +#align wcovby.snd WCovBy.snd -theorem mk_wcovby_mk_iff_left : (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂ := by - refine' ⟨Wcovby.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => _⟩ +theorem mk_wcovBy_mk_iff_left : (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂ := by + refine' ⟨WCovBy.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => _⟩ have : c.2 = b := h₂.le.2.antisymm h₁.le.2 rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂ exact h h₁ h₂ -#align prod.mk_wcovby_mk_iff_left Prod.mk_wcovby_mk_iff_left +#align prod.mk_wcovby_mk_iff_left Prod.mk_wcovBy_mk_iff_left -theorem mk_wcovby_mk_iff_right : (a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂ := - swap_wcovby_swap.trans mk_wcovby_mk_iff_left -#align prod.mk_wcovby_mk_iff_right Prod.mk_wcovby_mk_iff_right +theorem mk_wcovBy_mk_iff_right : (a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂ := + swap_wcovBy_swap.trans mk_wcovBy_mk_iff_left +#align prod.mk_wcovby_mk_iff_right Prod.mk_wcovBy_mk_iff_right -theorem mk_covby_mk_iff_left : (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂ := by - simp_rw [covby_iff_wcovby_and_lt, mk_wcovby_mk_iff_left, mk_lt_mk_iff_left] -#align prod.mk_covby_mk_iff_left Prod.mk_covby_mk_iff_left +theorem mk_covBy_mk_iff_left : (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂ := by + simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_left, mk_lt_mk_iff_left] +#align prod.mk_covby_mk_iff_left Prod.mk_covBy_mk_iff_left -theorem mk_covby_mk_iff_right : (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂ := by - simp_rw [covby_iff_wcovby_and_lt, mk_wcovby_mk_iff_right, mk_lt_mk_iff_right] -#align prod.mk_covby_mk_iff_right Prod.mk_covby_mk_iff_right +theorem mk_covBy_mk_iff_right : (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂ := by + simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_right, mk_lt_mk_iff_right] +#align prod.mk_covby_mk_iff_right Prod.mk_covBy_mk_iff_right -theorem mk_wcovby_mk_iff : (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ := by +theorem mk_wcovBy_mk_iff : (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ := by refine' ⟨fun h => _, _⟩ - · obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovby h - · exact Or.inr ⟨mk_wcovby_mk_iff_right.1 h, rfl⟩ - · exact Or.inl ⟨mk_wcovby_mk_iff_left.1 h, rfl⟩ + · obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h + · exact Or.inr ⟨mk_wcovBy_mk_iff_right.1 h, rfl⟩ + · exact Or.inl ⟨mk_wcovBy_mk_iff_left.1 h, rfl⟩ · rintro (⟨h, rfl⟩ | ⟨h, rfl⟩) - · exact mk_wcovby_mk_iff_left.2 h - · exact mk_wcovby_mk_iff_right.2 h -#align prod.mk_wcovby_mk_iff Prod.mk_wcovby_mk_iff + · exact mk_wcovBy_mk_iff_left.2 h + · exact mk_wcovBy_mk_iff_right.2 h +#align prod.mk_wcovby_mk_iff Prod.mk_wcovBy_mk_iff -theorem mk_covby_mk_iff : (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ := by +theorem mk_covBy_mk_iff : (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ := by refine' ⟨fun h => _, _⟩ - · obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovby h.wcovby - · exact Or.inr ⟨mk_covby_mk_iff_right.1 h, rfl⟩ - · exact Or.inl ⟨mk_covby_mk_iff_left.1 h, rfl⟩ + · obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h.wcovBy + · exact Or.inr ⟨mk_covBy_mk_iff_right.1 h, rfl⟩ + · exact Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩ · rintro (⟨h, rfl⟩ | ⟨h, rfl⟩) - · exact mk_covby_mk_iff_left.2 h - · exact mk_covby_mk_iff_right.2 h -#align prod.mk_covby_mk_iff Prod.mk_covby_mk_iff + · exact mk_covBy_mk_iff_left.2 h + · exact mk_covBy_mk_iff_right.2 h +#align prod.mk_covby_mk_iff Prod.mk_covBy_mk_iff -theorem wcovby_iff : x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1 := by +theorem wcovBy_iff : x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1 := by cases x cases y - exact mk_wcovby_mk_iff -#align prod.wcovby_iff Prod.wcovby_iff + exact mk_wcovBy_mk_iff +#align prod.wcovby_iff Prod.wcovBy_iff -theorem covby_iff : x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 := by +theorem covBy_iff : x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 := by cases x cases y - exact mk_covby_mk_iff -#align prod.covby_iff Prod.covby_iff + exact mk_covBy_mk_iff +#align prod.covby_iff Prod.covBy_iff end Prod diff --git a/Mathlib/Order/Grade.lean b/Mathlib/Order/Grade.lean index 01c1a6246dc9b..4f2d372999f30 100644 --- a/Mathlib/Order/Grade.lean +++ b/Mathlib/Order/Grade.lean @@ -61,14 +61,14 @@ open Finset Nat OrderDual variable {𝕆 ℙ α β : Type*} /-- An `𝕆`-graded order is an order `α` equipped with a strictly monotone function -`grade 𝕆 : α → 𝕆` which preserves order covering (`Covby`). -/ +`grade 𝕆 : α → 𝕆` which preserves order covering (`CovBy`). -/ class GradeOrder (𝕆 α : Type*) [Preorder 𝕆] [Preorder α] where /-- The grading function. -/ grade : α → 𝕆 /-- `grade` is strictly monotonic. -/ grade_strictMono : StrictMono grade - /-- `grade` preserves `Covby`. -/ - covby_grade ⦃a b : α⦄ : a ⋖ b → grade a ⋖ grade b + /-- `grade` preserves `CovBy`. -/ + covBy_grade ⦃a b : α⦄ : a ⋖ b → grade a ⋖ grade b #align grade_order GradeOrder /-- An `𝕆`-graded order where minimal elements have minimal grades. -/ @@ -105,9 +105,9 @@ def grade : α → 𝕆 := GradeOrder.grade #align grade grade -protected theorem Covby.grade (h : a ⋖ b) : grade 𝕆 a ⋖ grade 𝕆 b := - GradeOrder.covby_grade h -#align covby.grade Covby.grade +protected theorem CovBy.grade (h : a ⋖ b) : grade 𝕆 a ⋖ grade 𝕆 b := + GradeOrder.covBy_grade h +#align covby.grade CovBy.grade variable {𝕆} @@ -115,10 +115,10 @@ theorem grade_strictMono : StrictMono (grade 𝕆 : α → 𝕆) := GradeOrder.grade_strictMono #align grade_strict_mono grade_strictMono -theorem covby_iff_lt_covby_grade : a ⋖ b ↔ a < b ∧ grade 𝕆 a ⋖ grade 𝕆 b := +theorem covBy_iff_lt_covBy_grade : a ⋖ b ↔ a < b ∧ grade 𝕆 a ⋖ grade 𝕆 b := ⟨fun h => ⟨h.1, h.grade _⟩, And.imp_right fun h _ ha hb => h.2 (grade_strictMono ha) <| grade_strictMono hb⟩ -#align covby_iff_lt_covby_grade covby_iff_lt_covby_grade +#align covby_iff_lt_covby_grade covBy_iff_lt_covBy_grade end GradeOrder @@ -191,9 +191,9 @@ theorem grade_ne_grade_iff : grade 𝕆 a ≠ grade 𝕆 b ↔ a ≠ b := grade_injective.ne_iff #align grade_ne_grade_iff grade_ne_grade_iff -theorem grade_covby_grade_iff : grade 𝕆 a ⋖ grade 𝕆 b ↔ a ⋖ b := - (covby_iff_lt_covby_grade.trans <| and_iff_right_of_imp fun h => grade_lt_grade_iff.1 h.1).symm -#align grade_covby_grade_iff grade_covby_grade_iff +theorem grade_covBy_grade_iff : grade 𝕆 a ⋖ grade 𝕆 b ↔ a ⋖ b := + (covBy_iff_lt_covBy_grade.trans <| and_iff_right_of_imp fun h => grade_lt_grade_iff.1 h.1).symm +#align grade_covby_grade_iff grade_covBy_grade_iff end LinearOrder @@ -226,7 +226,7 @@ instance Preorder.toGradeBoundedOrder : GradeBoundedOrder α α where isMin_grade _ := id isMax_grade _ := id grade_strictMono := strictMono_id - covby_grade _ _ := id + covBy_grade _ _ := id #align preorder.to_grade_bounded_order Preorder.toGradeBoundedOrder @[simp] @@ -239,7 +239,7 @@ theorem grade_self (a : α) : grade α a = a := instance OrderDual.gradeOrder [GradeOrder 𝕆 α] : GradeOrder 𝕆ᵒᵈ αᵒᵈ where grade := toDual ∘ grade 𝕆 ∘ ofDual grade_strictMono := grade_strictMono.dual - covby_grade _ _ h := (h.ofDual.grade _).toDual + covBy_grade _ _ h := (h.ofDual.grade _).toDual instance OrderDual.gradeMinOrder [GradeMaxOrder 𝕆 α] : GradeMinOrder 𝕆ᵒᵈ αᵒᵈ := { OrderDual.gradeOrder with isMin_grade := fun _ => IsMax.grade (α := α) 𝕆 } @@ -266,72 +266,72 @@ theorem grade_ofDual [GradeOrder 𝕆 α] (a : αᵒᵈ) : grade 𝕆 (ofDual a) /-- Lifts a graded order along a strictly monotone function. -/ @[reducible] def GradeOrder.liftLeft [GradeOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) - (hcovby : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder ℙ α + (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder ℙ α where grade := f ∘ (@grade 𝕆 _ _ _ _) -- porting note - what the hell?! used to be `grade 𝕆` grade_strictMono := hf.comp grade_strictMono - covby_grade _ _ h := hcovby _ _ <| h.grade _ + covBy_grade _ _ h := hcovBy _ _ <| h.grade _ #align grade_order.lift_left GradeOrder.liftLeft -- See note [reducible non-instances] /-- Lifts a graded order along a strictly monotone function. -/ @[reducible] def GradeMinOrder.liftLeft [GradeMinOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) - (hcovby : ∀ a b, a ⋖ b → f a ⋖ f b) (hmin : ∀ a, IsMin a → IsMin (f a)) : GradeMinOrder ℙ α := - { GradeOrder.liftLeft f hf hcovby with isMin_grade := fun _ ha => hmin _ <| ha.grade _ } + (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) (hmin : ∀ a, IsMin a → IsMin (f a)) : GradeMinOrder ℙ α := + { GradeOrder.liftLeft f hf hcovBy with isMin_grade := fun _ ha => hmin _ <| ha.grade _ } #align grade_min_order.lift_left GradeMinOrder.liftLeft -- See note [reducible non-instances] /-- Lifts a graded order along a strictly monotone function. -/ @[reducible] def GradeMaxOrder.liftLeft [GradeMaxOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) - (hcovby : ∀ a b, a ⋖ b → f a ⋖ f b) (hmax : ∀ a, IsMax a → IsMax (f a)) : GradeMaxOrder ℙ α := - { GradeOrder.liftLeft f hf hcovby with isMax_grade := fun _ ha => hmax _ <| ha.grade _ } + (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) (hmax : ∀ a, IsMax a → IsMax (f a)) : GradeMaxOrder ℙ α := + { GradeOrder.liftLeft f hf hcovBy with isMax_grade := fun _ ha => hmax _ <| ha.grade _ } #align grade_max_order.lift_left GradeMaxOrder.liftLeft -- See note [reducible non-instances] /-- Lifts a graded order along a strictly monotone function. -/ @[reducible] def GradeBoundedOrder.liftLeft [GradeBoundedOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) - (hcovby : ∀ a b, a ⋖ b → f a ⋖ f b) (hmin : ∀ a, IsMin a → IsMin (f a)) + (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) (hmin : ∀ a, IsMin a → IsMin (f a)) (hmax : ∀ a, IsMax a → IsMax (f a)) : GradeBoundedOrder ℙ α := - { GradeMinOrder.liftLeft f hf hcovby hmin, GradeMaxOrder.liftLeft f hf hcovby hmax with } + { GradeMinOrder.liftLeft f hf hcovBy hmin, GradeMaxOrder.liftLeft f hf hcovBy hmax with } #align grade_bounded_order.lift_left GradeBoundedOrder.liftLeft -- See note [reducible non-instances] /-- Lifts a graded order along a strictly monotone function. -/ @[reducible] def GradeOrder.liftRight [GradeOrder 𝕆 β] (f : α → β) (hf : StrictMono f) - (hcovby : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder 𝕆 α + (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder 𝕆 α where grade := (@grade 𝕆 _ _ _ _) ∘ f -- porting note: again, weird grade_strictMono := grade_strictMono.comp hf - covby_grade _ _ h := (hcovby _ _ h).grade _ + covBy_grade _ _ h := (hcovBy _ _ h).grade _ #align grade_order.lift_right GradeOrder.liftRight -- See note [reducible non-instances] /-- Lifts a graded order along a strictly monotone function. -/ @[reducible] def GradeMinOrder.liftRight [GradeMinOrder 𝕆 β] (f : α → β) (hf : StrictMono f) - (hcovby : ∀ a b, a ⋖ b → f a ⋖ f b) (hmin : ∀ a, IsMin a → IsMin (f a)) : GradeMinOrder 𝕆 α := - { GradeOrder.liftRight f hf hcovby with isMin_grade := fun _ ha => (hmin _ ha).grade _ } + (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) (hmin : ∀ a, IsMin a → IsMin (f a)) : GradeMinOrder 𝕆 α := + { GradeOrder.liftRight f hf hcovBy with isMin_grade := fun _ ha => (hmin _ ha).grade _ } #align grade_min_order.lift_right GradeMinOrder.liftRight -- See note [reducible non-instances] /-- Lifts a graded order along a strictly monotone function. -/ @[reducible] def GradeMaxOrder.liftRight [GradeMaxOrder 𝕆 β] (f : α → β) (hf : StrictMono f) - (hcovby : ∀ a b, a ⋖ b → f a ⋖ f b) (hmax : ∀ a, IsMax a → IsMax (f a)) : GradeMaxOrder 𝕆 α := - { GradeOrder.liftRight f hf hcovby with isMax_grade := fun _ ha => (hmax _ ha).grade _ } + (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) (hmax : ∀ a, IsMax a → IsMax (f a)) : GradeMaxOrder 𝕆 α := + { GradeOrder.liftRight f hf hcovBy with isMax_grade := fun _ ha => (hmax _ ha).grade _ } #align grade_max_order.lift_right GradeMaxOrder.liftRight -- See note [reducible non-instances] /-- Lifts a graded order along a strictly monotone function. -/ @[reducible] def GradeBoundedOrder.liftRight [GradeBoundedOrder 𝕆 β] (f : α → β) (hf : StrictMono f) - (hcovby : ∀ a b, a ⋖ b → f a ⋖ f b) (hmin : ∀ a, IsMin a → IsMin (f a)) + (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) (hmin : ∀ a, IsMin a → IsMin (f a)) (hmax : ∀ a, IsMax a → IsMax (f a)) : GradeBoundedOrder 𝕆 α := - { GradeMinOrder.liftRight f hf hcovby hmin, GradeMaxOrder.liftRight f hf hcovby hmax with } + { GradeMinOrder.liftRight f hf hcovBy hmin, GradeMaxOrder.liftRight f hf hcovBy hmax with } #align grade_bounded_order.lift_right GradeBoundedOrder.liftRight /-! #### `Fin n`-graded to `ℕ`-graded to `ℤ`-graded -/ @@ -342,7 +342,7 @@ def GradeBoundedOrder.liftRight [GradeBoundedOrder 𝕆 β] (f : α → β) (hf inferrable. -/ @[reducible] def GradeOrder.finToNat (n : ℕ) [GradeOrder (Fin n) α] : GradeOrder ℕ α := - (GradeOrder.liftLeft (_ : Fin n → ℕ) Fin.val_strictMono) fun _ _ => Covby.coe_fin + (GradeOrder.liftLeft (_ : Fin n → ℕ) Fin.val_strictMono) fun _ _ => CovBy.coe_fin #align grade_order.fin_to_nat GradeOrder.finToNat -- See note [reducible non-instances] @@ -350,7 +350,7 @@ def GradeOrder.finToNat (n : ℕ) [GradeOrder (Fin n) α] : GradeOrder ℕ α := inferrable. -/ @[reducible] def GradeMinOrder.finToNat (n : ℕ) [GradeMinOrder (Fin n) α] : GradeMinOrder ℕ α := - (GradeMinOrder.liftLeft (_ : Fin n → ℕ) Fin.val_strictMono fun _ _ => Covby.coe_fin) fun a h => by + (GradeMinOrder.liftLeft (_ : Fin n → ℕ) Fin.val_strictMono fun _ _ => CovBy.coe_fin) fun a h => by cases n · exact a.elim0 rw [h.eq_bot, Fin.bot_eq_zero] @@ -358,5 +358,5 @@ def GradeMinOrder.finToNat (n : ℕ) [GradeMinOrder (Fin n) α] : GradeMinOrder #align grade_min_order.fin_to_nat GradeMinOrder.finToNat instance GradeOrder.natToInt [GradeOrder ℕ α] : GradeOrder ℤ α := - (GradeOrder.liftLeft _ Int.coe_nat_strictMono) fun _ _ => Covby.cast_int + (GradeOrder.liftLeft _ Int.coe_nat_strictMono) fun _ _ => CovBy.cast_int #align grade_order.nat_to_int GradeOrder.natToInt diff --git a/Mathlib/Order/ModularLattice.lean b/Mathlib/Order/ModularLattice.lean index e6f4a6236245f..046c26bf2461e 100644 --- a/Mathlib/Order/ModularLattice.lean +++ b/Mathlib/Order/ModularLattice.lean @@ -61,28 +61,28 @@ variable {α : Type*} cover `a ⊓ b`. -/ class IsWeakUpperModularLattice (α : Type*) [Lattice α] : Prop where /-- `a ⊔ b` covers `a` and `b` if `a` and `b` both cover `a ⊓ b`. -/ - covby_sup_of_inf_covby_covby {a b : α} : a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b + covBy_sup_of_inf_covBy_covBy {a b : α} : a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b #align is_weak_upper_modular_lattice IsWeakUpperModularLattice /-- A weakly lower modular lattice is a lattice where `a` and `b` cover `a ⊓ b` if `a ⊔ b` covers both `a` and `b`. -/ class IsWeakLowerModularLattice (α : Type*) [Lattice α] : Prop where /-- `a` and `b` cover `a ⊓ b` if `a ⊔ b` covers both `a` and `b` -/ - inf_covby_of_covby_covby_sup {a b : α} : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a + inf_covBy_of_covBy_covBy_sup {a b : α} : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a #align is_weak_lower_modular_lattice IsWeakLowerModularLattice /-- An upper modular lattice, aka semimodular lattice, is a lattice where `a ⊔ b` covers `a` and `b` if either `a` or `b` covers `a ⊓ b`. -/ class IsUpperModularLattice (α : Type*) [Lattice α] : Prop where /-- `a ⊔ b` covers `a` and `b` if either `a` or `b` covers `a ⊓ b` -/ - covby_sup_of_inf_covby {a b : α} : a ⊓ b ⋖ a → b ⋖ a ⊔ b + covBy_sup_of_inf_covBy {a b : α} : a ⊓ b ⋖ a → b ⋖ a ⊔ b #align is_upper_modular_lattice IsUpperModularLattice /-- A lower modular lattice is a lattice where `a` and `b` both cover `a ⊓ b` if `a ⊔ b` covers either `a` or `b`. -/ class IsLowerModularLattice (α : Type*) [Lattice α] : Prop where /-- `a` and `b` both cover `a ⊓ b` if `a ⊔ b` covers either `a` or `b` -/ - inf_covby_of_covby_sup {a b : α} : a ⋖ a ⊔ b → a ⊓ b ⋖ b + inf_covBy_of_covBy_sup {a b : α} : a ⋖ a ⊔ b → a ⊓ b ⋖ b #align is_lower_modular_lattice IsLowerModularLattice /-- A modular lattice is one with a limited associativity between `⊓` and `⊔`. -/ @@ -95,20 +95,20 @@ section WeakUpperModular variable [Lattice α] [IsWeakUpperModularLattice α] {a b : α} -theorem covby_sup_of_inf_covby_of_inf_covby_left : a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b := - IsWeakUpperModularLattice.covby_sup_of_inf_covby_covby -#align covby_sup_of_inf_covby_of_inf_covby_left covby_sup_of_inf_covby_of_inf_covby_left +theorem covBy_sup_of_inf_covBy_of_inf_covBy_left : a ⊓ b ⋖ a → a ⊓ b ⋖ b → a ⋖ a ⊔ b := + IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy +#align covby_sup_of_inf_covby_of_inf_covby_left covBy_sup_of_inf_covBy_of_inf_covBy_left -theorem covby_sup_of_inf_covby_of_inf_covby_right : a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b := by +theorem covBy_sup_of_inf_covBy_of_inf_covBy_right : a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b := by rw [inf_comm, sup_comm] - exact fun ha hb => covby_sup_of_inf_covby_of_inf_covby_left hb ha -#align covby_sup_of_inf_covby_of_inf_covby_right covby_sup_of_inf_covby_of_inf_covby_right + exact fun ha hb => covBy_sup_of_inf_covBy_of_inf_covBy_left hb ha +#align covby_sup_of_inf_covby_of_inf_covby_right covBy_sup_of_inf_covBy_of_inf_covBy_right -alias Covby.sup_of_inf_of_inf_left := covby_sup_of_inf_covby_of_inf_covby_left -#align covby.sup_of_inf_of_inf_left Covby.sup_of_inf_of_inf_left +alias CovBy.sup_of_inf_of_inf_left := covBy_sup_of_inf_covBy_of_inf_covBy_left +#align covby.sup_of_inf_of_inf_left CovBy.sup_of_inf_of_inf_left -alias Covby.sup_of_inf_of_inf_right := covby_sup_of_inf_covby_of_inf_covby_right -#align covby.sup_of_inf_of_inf_right Covby.sup_of_inf_of_inf_right +alias CovBy.sup_of_inf_of_inf_right := covBy_sup_of_inf_covBy_of_inf_covBy_right +#align covby.sup_of_inf_of_inf_right CovBy.sup_of_inf_of_inf_right instance : IsWeakLowerModularLattice (OrderDual α) := ⟨fun ha hb => (ha.ofDual.sup_of_inf_of_inf_left hb.ofDual).toDual⟩ @@ -119,20 +119,20 @@ section WeakLowerModular variable [Lattice α] [IsWeakLowerModularLattice α] {a b : α} -theorem inf_covby_of_covby_sup_of_covby_sup_left : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a := - IsWeakLowerModularLattice.inf_covby_of_covby_covby_sup -#align inf_covby_of_covby_sup_of_covby_sup_left inf_covby_of_covby_sup_of_covby_sup_left +theorem inf_covBy_of_covBy_sup_of_covBy_sup_left : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a := + IsWeakLowerModularLattice.inf_covBy_of_covBy_covBy_sup +#align inf_covby_of_covby_sup_of_covby_sup_left inf_covBy_of_covBy_sup_of_covBy_sup_left -theorem inf_covby_of_covby_sup_of_covby_sup_right : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b := by +theorem inf_covBy_of_covBy_sup_of_covBy_sup_right : a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b := by rw [sup_comm, inf_comm] - exact fun ha hb => inf_covby_of_covby_sup_of_covby_sup_left hb ha -#align inf_covby_of_covby_sup_of_covby_sup_right inf_covby_of_covby_sup_of_covby_sup_right + exact fun ha hb => inf_covBy_of_covBy_sup_of_covBy_sup_left hb ha +#align inf_covby_of_covby_sup_of_covby_sup_right inf_covBy_of_covBy_sup_of_covBy_sup_right -alias Covby.inf_of_sup_of_sup_left := inf_covby_of_covby_sup_of_covby_sup_left -#align covby.inf_of_sup_of_sup_left Covby.inf_of_sup_of_sup_left +alias CovBy.inf_of_sup_of_sup_left := inf_covBy_of_covBy_sup_of_covBy_sup_left +#align covby.inf_of_sup_of_sup_left CovBy.inf_of_sup_of_sup_left -alias Covby.inf_of_sup_of_sup_right := inf_covby_of_covby_sup_of_covby_sup_right -#align covby.inf_of_sup_of_sup_right Covby.inf_of_sup_of_sup_right +alias CovBy.inf_of_sup_of_sup_right := inf_covBy_of_covBy_sup_of_covBy_sup_right +#align covby.inf_of_sup_of_sup_right CovBy.inf_of_sup_of_sup_right instance : IsWeakUpperModularLattice (OrderDual α) := ⟨fun ha hb => (ha.ofDual.inf_of_sup_of_sup_left hb.ofDual).toDual⟩ @@ -143,25 +143,25 @@ section UpperModular variable [Lattice α] [IsUpperModularLattice α] {a b : α} -theorem covby_sup_of_inf_covby_left : a ⊓ b ⋖ a → b ⋖ a ⊔ b := - IsUpperModularLattice.covby_sup_of_inf_covby -#align covby_sup_of_inf_covby_left covby_sup_of_inf_covby_left +theorem covBy_sup_of_inf_covBy_left : a ⊓ b ⋖ a → b ⋖ a ⊔ b := + IsUpperModularLattice.covBy_sup_of_inf_covBy +#align covby_sup_of_inf_covby_left covBy_sup_of_inf_covBy_left -theorem covby_sup_of_inf_covby_right : a ⊓ b ⋖ b → a ⋖ a ⊔ b := by +theorem covBy_sup_of_inf_covBy_right : a ⊓ b ⋖ b → a ⋖ a ⊔ b := by rw [sup_comm, inf_comm] - exact covby_sup_of_inf_covby_left -#align covby_sup_of_inf_covby_right covby_sup_of_inf_covby_right + exact covBy_sup_of_inf_covBy_left +#align covby_sup_of_inf_covby_right covBy_sup_of_inf_covBy_right -alias Covby.sup_of_inf_left := covby_sup_of_inf_covby_left -#align covby.sup_of_inf_left Covby.sup_of_inf_left +alias CovBy.sup_of_inf_left := covBy_sup_of_inf_covBy_left +#align covby.sup_of_inf_left CovBy.sup_of_inf_left -alias Covby.sup_of_inf_right := covby_sup_of_inf_covby_right -#align covby.sup_of_inf_right Covby.sup_of_inf_right +alias CovBy.sup_of_inf_right := covBy_sup_of_inf_covBy_right +#align covby.sup_of_inf_right CovBy.sup_of_inf_right -- See note [lower instance priority] instance (priority := 100) IsUpperModularLattice.to_isWeakUpperModularLattice : IsWeakUpperModularLattice α := - ⟨fun _ => Covby.sup_of_inf_right⟩ + ⟨fun _ => CovBy.sup_of_inf_right⟩ #align is_upper_modular_lattice.to_is_weak_upper_modular_lattice IsUpperModularLattice.to_isWeakUpperModularLattice instance : IsLowerModularLattice (OrderDual α) := @@ -173,25 +173,25 @@ section LowerModular variable [Lattice α] [IsLowerModularLattice α] {a b : α} -theorem inf_covby_of_covby_sup_left : a ⋖ a ⊔ b → a ⊓ b ⋖ b := - IsLowerModularLattice.inf_covby_of_covby_sup -#align inf_covby_of_covby_sup_left inf_covby_of_covby_sup_left +theorem inf_covBy_of_covBy_sup_left : a ⋖ a ⊔ b → a ⊓ b ⋖ b := + IsLowerModularLattice.inf_covBy_of_covBy_sup +#align inf_covby_of_covby_sup_left inf_covBy_of_covBy_sup_left -theorem inf_covby_of_covby_sup_right : b ⋖ a ⊔ b → a ⊓ b ⋖ a := by +theorem inf_covBy_of_covBy_sup_right : b ⋖ a ⊔ b → a ⊓ b ⋖ a := by rw [inf_comm, sup_comm] - exact inf_covby_of_covby_sup_left -#align inf_covby_of_covby_sup_right inf_covby_of_covby_sup_right + exact inf_covBy_of_covBy_sup_left +#align inf_covby_of_covby_sup_right inf_covBy_of_covBy_sup_right -alias Covby.inf_of_sup_left := inf_covby_of_covby_sup_left -#align covby.inf_of_sup_left Covby.inf_of_sup_left +alias CovBy.inf_of_sup_left := inf_covBy_of_covBy_sup_left +#align covby.inf_of_sup_left CovBy.inf_of_sup_left -alias Covby.inf_of_sup_right := inf_covby_of_covby_sup_right -#align covby.inf_of_sup_right Covby.inf_of_sup_right +alias CovBy.inf_of_sup_right := inf_covBy_of_covBy_sup_right +#align covby.inf_of_sup_right CovBy.inf_of_sup_right -- See note [lower instance priority] instance (priority := 100) IsLowerModularLattice.to_isWeakLowerModularLattice : IsWeakLowerModularLattice α := - ⟨fun _ => Covby.inf_of_sup_right⟩ + ⟨fun _ => CovBy.inf_of_sup_right⟩ #align is_lower_modular_lattice.to_is_weak_lower_modular_lattice IsLowerModularLattice.to_isWeakLowerModularLattice instance : IsUpperModularLattice (OrderDual α) := @@ -346,7 +346,7 @@ def infIooOrderIsoIooSup (a b : α) : Ioo (a ⊓ b) a ≃o Ioo b (a ⊔ b) where -- See note [lower instance priority] instance (priority := 100) IsModularLattice.to_isLowerModularLattice : IsLowerModularLattice α := ⟨fun {a b} => by - simp_rw [covby_iff_Ioo_eq, @sup_comm _ _ a, @inf_comm _ _ a, ← isEmpty_coe_sort, right_lt_sup, + simp_rw [covBy_iff_Ioo_eq, @sup_comm _ _ a, @inf_comm _ _ a, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left, (infIooOrderIsoIooSup b a).symm.toEquiv.isEmpty_congr] exact id⟩ #align is_modular_lattice.to_is_lower_modular_lattice IsModularLattice.to_isLowerModularLattice @@ -354,7 +354,7 @@ instance (priority := 100) IsModularLattice.to_isLowerModularLattice : IsLowerMo -- See note [lower instance priority] instance (priority := 100) IsModularLattice.to_isUpperModularLattice : IsUpperModularLattice α := ⟨fun {a b} => by - simp_rw [covby_iff_Ioo_eq, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left, + simp_rw [covBy_iff_Ioo_eq, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left, (infIooOrderIsoIooSup a b).toEquiv.isEmpty_congr] exact id⟩ #align is_modular_lattice.to_is_upper_modular_lattice IsModularLattice.to_isUpperModularLattice diff --git a/Mathlib/Order/SuccPred/Basic.lean b/Mathlib/Order/SuccPred/Basic.lean index c01f09bf95643..d0a546046e186 100644 --- a/Mathlib/Order/SuccPred/Basic.lean +++ b/Mathlib/Order/SuccPred/Basic.lean @@ -50,7 +50,7 @@ Is `GaloisConnection pred succ` always true? If not, we should introduce class SuccPredOrder (α : Type*) [Preorder α] extends SuccOrder α, PredOrder α := (pred_succ_gc : GaloisConnection (pred : α → α) succ) ``` -`Covby` should help here. +`CovBy` should help here. -/ @@ -239,13 +239,13 @@ theorem lt_succ_iff_not_isMax : a < succ a ↔ ¬IsMax a := alias ⟨_, lt_succ_of_not_isMax⟩ := lt_succ_iff_not_isMax #align order.lt_succ_of_not_is_max Order.lt_succ_of_not_isMax -theorem wcovby_succ (a : α) : a ⩿ succ a := +theorem wcovBy_succ (a : α) : a ⩿ succ a := ⟨le_succ a, fun _ hb => (succ_le_of_lt hb).not_lt⟩ -#align order.wcovby_succ Order.wcovby_succ +#align order.wcovby_succ Order.wcovBy_succ -theorem covby_succ_of_not_isMax (h : ¬IsMax a) : a ⋖ succ a := - (wcovby_succ a).covby_of_lt <| lt_succ_of_not_isMax h -#align order.covby_succ_of_not_is_max Order.covby_succ_of_not_isMax +theorem covBy_succ_of_not_isMax (h : ¬IsMax a) : a ⋖ succ a := + (wcovBy_succ a).covBy_of_lt <| lt_succ_of_not_isMax h +#align order.covby_succ_of_not_is_max Order.covBy_succ_of_not_isMax theorem lt_succ_iff_of_not_isMax (ha : ¬IsMax a) : b < succ a ↔ b ≤ a := ⟨le_of_lt_succ, fun h => h.trans_lt <| lt_succ_of_not_isMax ha⟩ @@ -360,9 +360,9 @@ alias ⟨lt_of_succ_lt_succ, succ_lt_succ⟩ := succ_lt_succ_iff theorem succ_strictMono : StrictMono (succ : α → α) := fun _ _ => succ_lt_succ #align order.succ_strict_mono Order.succ_strictMono -theorem covby_succ (a : α) : a ⋖ succ a := - covby_succ_of_not_isMax <| not_isMax a -#align order.covby_succ Order.covby_succ +theorem covBy_succ (a : α) : a ⋖ succ a := + covBy_succ_of_not_isMax <| not_isMax a +#align order.covby_succ Order.covBy_succ @[simp] theorem Iio_succ (a : α) : Iio (succ a) = Iic a := @@ -427,15 +427,15 @@ theorem le_le_succ_iff : a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a := by · exact ⟨le_succ a, le_rfl⟩ #align order.le_le_succ_iff Order.le_le_succ_iff -theorem _root_.Covby.succ_eq (h : a ⋖ b) : succ a = b := +theorem _root_.CovBy.succ_eq (h : a ⋖ b) : succ a = b := (succ_le_of_lt h.lt).eq_of_not_lt fun h' => h.2 (lt_succ_of_not_isMax h.lt.not_isMax) h' -#align covby.succ_eq Covby.succ_eq +#align covby.succ_eq CovBy.succ_eq -theorem _root_.Wcovby.le_succ (h : a ⩿ b) : b ≤ succ a := by - obtain h | rfl := h.covby_or_eq - · exact (Covby.succ_eq h).ge +theorem _root_.WCovBy.le_succ (h : a ⩿ b) : b ≤ succ a := by + obtain h | rfl := h.covBy_or_eq + · exact (CovBy.succ_eq h).ge · exact le_succ _ -#align wcovby.le_succ Wcovby.le_succ +#align wcovby.le_succ WCovBy.le_succ theorem le_succ_iff_eq_or_le : a ≤ succ b ↔ a = succ b ∨ a ≤ b := by by_cases hb : IsMax b @@ -496,11 +496,11 @@ theorem lt_succ_iff_eq_or_lt : a < succ b ↔ a = b ∨ a < b := lt_succ_iff.trans le_iff_eq_or_lt #align order.lt_succ_iff_eq_or_lt Order.lt_succ_iff_eq_or_lt -theorem succ_eq_iff_covby : succ a = b ↔ a ⋖ b := +theorem succ_eq_iff_covBy : succ a = b ↔ a ⋖ b := ⟨by rintro rfl - exact covby_succ _, Covby.succ_eq⟩ -#align order.succ_eq_iff_covby Order.succ_eq_iff_covby + exact covBy_succ _, CovBy.succ_eq⟩ +#align order.succ_eq_iff_covby Order.succ_eq_iff_covBy theorem Iio_succ_eq_insert (a : α) : Iio (succ a) = insert a (Iio a) := Iio_succ_eq_insert_of_not_isMax <| not_isMax a @@ -570,7 +570,7 @@ instance [PartialOrder α] : Subsingleton (SuccOrder α) := ext a by_cases ha : IsMax a · exact (@IsMax.succ_eq _ _ h₀ _ ha).trans ha.succ_eq.symm - · exact @Covby.succ_eq _ _ h₀ _ _ (covby_succ_of_not_isMax ha)⟩ + · exact @CovBy.succ_eq _ _ h₀ _ _ (covBy_succ_of_not_isMax ha)⟩ section CompleteLattice @@ -627,13 +627,13 @@ theorem pred_lt_iff_not_isMin : pred a < a ↔ ¬IsMin a := alias ⟨_, pred_lt_of_not_isMin⟩ := pred_lt_iff_not_isMin #align order.pred_lt_of_not_is_min Order.pred_lt_of_not_isMin -theorem pred_wcovby (a : α) : pred a ⩿ a := +theorem pred_wcovBy (a : α) : pred a ⩿ a := ⟨pred_le a, fun _ hb => (le_of_pred_lt hb).not_lt⟩ -#align order.pred_wcovby Order.pred_wcovby +#align order.pred_wcovby Order.pred_wcovBy -theorem pred_covby_of_not_isMin (h : ¬IsMin a) : pred a ⋖ a := - (pred_wcovby a).covby_of_lt <| pred_lt_of_not_isMin h -#align order.pred_covby_of_not_is_min Order.pred_covby_of_not_isMin +theorem pred_covBy_of_not_isMin (h : ¬IsMin a) : pred a ⋖ a := + (pred_wcovBy a).covBy_of_lt <| pred_lt_of_not_isMin h +#align order.pred_covby_of_not_is_min Order.pred_covBy_of_not_isMin theorem pred_lt_iff_of_not_isMin (ha : ¬IsMin a) : pred a < b ↔ a ≤ b := ⟨le_of_pred_lt, (pred_lt_of_not_isMin ha).trans_le⟩ @@ -727,9 +727,9 @@ alias ⟨lt_of_pred_lt_pred, pred_lt_pred⟩ := pred_lt_pred_iff theorem pred_strictMono : StrictMono (pred : α → α) := fun _ _ => pred_lt_pred #align order.pred_strict_mono Order.pred_strictMono -theorem pred_covby (a : α) : pred a ⋖ a := - pred_covby_of_not_isMin <| not_isMin a -#align order.pred_covby Order.pred_covby +theorem pred_covBy (a : α) : pred a ⋖ a := + pred_covBy_of_not_isMin <| not_isMin a +#align order.pred_covby Order.pred_covBy @[simp] theorem Ioi_pred (a : α) : Ioi (pred a) = Ici a := @@ -786,15 +786,15 @@ theorem pred_le_le_iff {a b : α} : pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = p · exact ⟨le_rfl, pred_le a⟩ #align order.pred_le_le_iff Order.pred_le_le_iff -theorem _root_.Covby.pred_eq {a b : α} (h : a ⋖ b) : pred b = a := +theorem _root_.CovBy.pred_eq {a b : α} (h : a ⋖ b) : pred b = a := (le_pred_of_lt h.lt).eq_of_not_gt fun h' => h.2 h' <| pred_lt_of_not_isMin h.lt.not_isMin -#align covby.pred_eq Covby.pred_eq +#align covby.pred_eq CovBy.pred_eq -theorem _root_.Wcovby.pred_le (h : a ⩿ b) : pred b ≤ a := by - obtain h | rfl := h.covby_or_eq - · exact (Covby.pred_eq h).le +theorem _root_.WCovBy.pred_le (h : a ⩿ b) : pred b ≤ a := by + obtain h | rfl := h.covBy_or_eq + · exact (CovBy.pred_eq h).le · exact pred_le _ -#align wcovby.pred_le Wcovby.pred_le +#align wcovby.pred_le WCovBy.pred_le theorem pred_le_iff_eq_or_le : pred a ≤ b ↔ b = pred a ∨ a ≤ b := by by_cases ha : IsMin a @@ -846,11 +846,11 @@ theorem pred_lt_iff_eq_or_lt : pred a < b ↔ a = b ∨ a < b := pred_lt_iff.trans le_iff_eq_or_lt #align order.pred_lt_iff_eq_or_lt Order.pred_lt_iff_eq_or_lt -theorem pred_eq_iff_covby : pred b = a ↔ a ⋖ b := +theorem pred_eq_iff_covBy : pred b = a ↔ a ⋖ b := ⟨by rintro rfl - exact pred_covby _, Covby.pred_eq⟩ -#align order.pred_eq_iff_covby Order.pred_eq_iff_covby + exact pred_covBy _, CovBy.pred_eq⟩ +#align order.pred_eq_iff_covby Order.pred_eq_iff_covBy theorem Ioi_pred_eq_insert (a : α) : Ioi (pred a) = insert a (Ioi a) := ext fun _ => pred_lt_iff_eq_or_lt.trans <| or_congr_left eq_comm @@ -921,7 +921,7 @@ instance [PartialOrder α] : Subsingleton (PredOrder α) := ext a by_cases ha : IsMin a · exact (@IsMin.pred_eq _ _ h₀ _ ha).trans ha.pred_eq.symm - · exact @Covby.pred_eq _ _ h₀ _ _ (pred_covby_of_not_isMin ha)⟩ + · exact @CovBy.pred_eq _ _ h₀ _ _ (pred_covBy_of_not_isMin ha)⟩ section CompleteLattice @@ -945,22 +945,22 @@ variable [PartialOrder α] [SuccOrder α] [PredOrder α] {a b : α} @[simp] theorem succ_pred_of_not_isMin (h : ¬IsMin a) : succ (pred a) = a := - Covby.succ_eq (pred_covby_of_not_isMin h) + CovBy.succ_eq (pred_covBy_of_not_isMin h) #align order.succ_pred_of_not_is_min Order.succ_pred_of_not_isMin @[simp] theorem pred_succ_of_not_isMax (h : ¬IsMax a) : pred (succ a) = a := - Covby.pred_eq (covby_succ_of_not_isMax h) + CovBy.pred_eq (covBy_succ_of_not_isMax h) #align order.pred_succ_of_not_is_max Order.pred_succ_of_not_isMax --Porting note: removing @[simp],`simp` can prove it theorem succ_pred [NoMinOrder α] (a : α) : succ (pred a) = a := - Covby.succ_eq (pred_covby _) + CovBy.succ_eq (pred_covBy _) #align order.succ_pred Order.succ_pred --Porting note: removing @[simp],`simp` can prove it theorem pred_succ [NoMaxOrder α] (a : α) : pred (succ a) = a := - Covby.pred_eq (covby_succ _) + CovBy.pred_eq (covBy_succ _) #align order.pred_succ Order.pred_succ theorem pred_succ_iterate_of_not_isMax (i : α) (n : ℕ) (hin : ¬IsMax (succ^[n - 1] i)) : diff --git a/Mathlib/Order/SuccPred/Limit.lean b/Mathlib/Order/SuccPred/Limit.lean index ad5197a673326..8b0a4a3f3598c 100644 --- a/Mathlib/Order/SuccPred/Limit.lean +++ b/Mathlib/Order/SuccPred/Limit.lean @@ -43,12 +43,12 @@ def IsSuccLimit (a : α) : Prop := ∀ b, ¬b ⋖ a #align order.is_succ_limit Order.IsSuccLimit -theorem not_isSuccLimit_iff_exists_covby (a : α) : ¬IsSuccLimit a ↔ ∃ b, b ⋖ a := by +theorem not_isSuccLimit_iff_exists_covBy (a : α) : ¬IsSuccLimit a ↔ ∃ b, b ⋖ a := by simp [IsSuccLimit] -#align order.not_is_succ_limit_iff_exists_covby Order.not_isSuccLimit_iff_exists_covby +#align order.not_is_succ_limit_iff_exists_covby Order.not_isSuccLimit_iff_exists_covBy @[simp] -theorem isSuccLimit_of_dense [DenselyOrdered α] (a : α) : IsSuccLimit a := fun _ => not_covby +theorem isSuccLimit_of_dense [DenselyOrdered α] (a : α) : IsSuccLimit a := fun _ => not_covBy #align order.is_succ_limit_of_dense Order.isSuccLimit_of_dense end LT @@ -69,7 +69,7 @@ variable [SuccOrder α] protected theorem IsSuccLimit.isMax (h : IsSuccLimit (succ a)) : IsMax a := by by_contra H - exact h a (covby_succ_of_not_isMax H) + exact h a (covBy_succ_of_not_isMax H) #align order.is_succ_limit.is_max Order.IsSuccLimit.isMax theorem not_isSuccLimit_succ_of_not_isMax (ha : ¬IsMax a) : ¬IsSuccLimit (succ a) := by @@ -120,14 +120,14 @@ section PartialOrder variable [PartialOrder α] [SuccOrder α] {a b : α} {C : α → Sort*} theorem isSuccLimit_of_succ_ne (h : ∀ b, succ b ≠ a) : IsSuccLimit a := fun b hba => - h b (Covby.succ_eq hba) + h b (CovBy.succ_eq hba) #align order.is_succ_limit_of_succ_ne Order.isSuccLimit_of_succ_ne theorem not_isSuccLimit_iff : ¬IsSuccLimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a := by - rw [not_isSuccLimit_iff_exists_covby] - refine' exists_congr fun b => ⟨fun hba => ⟨hba.lt.not_isMax, (Covby.succ_eq hba)⟩, _⟩ + rw [not_isSuccLimit_iff_exists_covBy] + refine' exists_congr fun b => ⟨fun hba => ⟨hba.lt.not_isMax, (CovBy.succ_eq hba)⟩, _⟩ rintro ⟨h, rfl⟩ - exact covby_succ_of_not_isMax h + exact covBy_succ_of_not_isMax h #align order.not_is_succ_limit_iff Order.not_isSuccLimit_iff /-- See `not_isSuccLimit_iff` for a version that states that `a` is a successor of a value other @@ -138,7 +138,7 @@ theorem mem_range_succ_of_not_isSuccLimit (h : ¬IsSuccLimit a) : a ∈ range (@ #align order.mem_range_succ_of_not_is_succ_limit Order.mem_range_succ_of_not_isSuccLimit theorem isSuccLimit_of_succ_lt (H : ∀ a < b, succ a < b) : IsSuccLimit b := fun a hab => - (H a hab.lt).ne (Covby.succ_eq hab) + (H a hab.lt).ne (CovBy.succ_eq hab) #align order.is_succ_limit_of_succ_lt Order.isSuccLimit_of_succ_lt theorem IsSuccLimit.succ_lt (hb : IsSuccLimit b) (ha : a < b) : succ a < b := by @@ -245,11 +245,11 @@ def IsPredLimit (a : α) : Prop := ∀ b, ¬a ⋖ b #align order.is_pred_limit Order.IsPredLimit -theorem not_isPredLimit_iff_exists_covby (a : α) : ¬IsPredLimit a ↔ ∃ b, a ⋖ b := by +theorem not_isPredLimit_iff_exists_covBy (a : α) : ¬IsPredLimit a ↔ ∃ b, a ⋖ b := by simp [IsPredLimit] -#align order.not_is_pred_limit_iff_exists_covby Order.not_isPredLimit_iff_exists_covby +#align order.not_is_pred_limit_iff_exists_covby Order.not_isPredLimit_iff_exists_covBy -theorem isPredLimit_of_dense [DenselyOrdered α] (a : α) : IsPredLimit a := fun _ => not_covby +theorem isPredLimit_of_dense [DenselyOrdered α] (a : α) : IsPredLimit a := fun _ => not_covBy #align order.is_pred_limit_of_dense Order.isPredLimit_of_dense @[simp] @@ -286,7 +286,7 @@ variable [PredOrder α] protected theorem IsPredLimit.isMin (h : IsPredLimit (pred a)) : IsMin a := by by_contra H - exact h a (pred_covby_of_not_isMin H) + exact h a (pred_covBy_of_not_isMin H) #align order.is_pred_limit.is_min Order.IsPredLimit.isMin theorem not_isPredLimit_pred_of_not_isMin (ha : ¬IsMin a) : ¬IsPredLimit (pred a) := by @@ -334,7 +334,7 @@ section PartialOrder variable [PartialOrder α] [PredOrder α] {a b : α} {C : α → Sort*} theorem isPredLimit_of_pred_ne (h : ∀ b, pred b ≠ a) : IsPredLimit a := fun b hba => - h b (Covby.pred_eq hba) + h b (CovBy.pred_eq hba) #align order.is_pred_limit_of_pred_ne Order.isPredLimit_of_pred_ne theorem not_isPredLimit_iff : ¬IsPredLimit a ↔ ∃ b, ¬IsMin b ∧ pred b = a := by @@ -350,7 +350,7 @@ theorem mem_range_pred_of_not_isPredLimit (h : ¬IsPredLimit a) : a ∈ range (@ #align order.mem_range_pred_of_not_is_pred_limit Order.mem_range_pred_of_not_isPredLimit theorem isPredLimit_of_pred_lt (H : ∀ a > b, pred a < b) : IsPredLimit b := fun a hab => - (H a hab.lt).ne (Covby.pred_eq hab) + (H a hab.lt).ne (CovBy.pred_eq hab) #align order.is_pred_limit_of_pred_lt Order.isPredLimit_of_pred_lt theorem IsPredLimit.lt_pred (h : IsPredLimit a) : a < b → a < pred b := diff --git a/Mathlib/RingTheory/SimpleModule.lean b/Mathlib/RingTheory/SimpleModule.lean index 77eba283dbee9..6f586bfc92c65 100644 --- a/Mathlib/RingTheory/SimpleModule.lean +++ b/Mathlib/RingTheory/SimpleModule.lean @@ -70,15 +70,15 @@ theorem isSimpleModule_iff_isCoatom : IsSimpleModule R (M ⧸ m) ↔ IsCoatom m exact Submodule.comapMkQRelIso m #align is_simple_module_iff_is_coatom isSimpleModule_iff_isCoatom -theorem covby_iff_quot_is_simple {A B : Submodule R M} (hAB : A ≤ B) : +theorem covBy_iff_quot_is_simple {A B : Submodule R M} (hAB : A ≤ B) : A ⋖ B ↔ IsSimpleModule R (B ⧸ Submodule.comap B.subtype A) := by set f : Submodule R B ≃o Set.Iic B := Submodule.MapSubtype.relIso B with hf - rw [covby_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf] + rw [covBy_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf] -- This used to be in the next `simp`, but we need `erw` after leanprover/lean4#2644 erw [RelIso.coe_fn_mk] simp [-OrderIso.isCoatom_iff, Submodule.MapSubtype.relIso, Submodule.map_comap_subtype, inf_eq_right.2 hAB] -#align covby_iff_quot_is_simple covby_iff_quot_is_simple +#align covby_iff_quot_is_simple covBy_iff_quot_is_simple namespace IsSimpleModule @@ -222,9 +222,9 @@ theorem second_iso {X Y : Submodule R M} (_ : X ⋖ X ⊔ Y) : instance instJordanHolderLattice : JordanHolderLattice (Submodule R M) where IsMaximal := (· ⋖ ·) - lt_of_isMaximal := Covby.lt - sup_eq_of_isMaximal hxz hyz := Wcovby.sup_eq hxz.wcovby hyz.wcovby - isMaximal_inf_left_of_isMaximal_sup := inf_covby_of_covby_sup_of_covby_sup_left + lt_of_isMaximal := CovBy.lt + sup_eq_of_isMaximal hxz hyz := WCovBy.sup_eq hxz.wcovBy hyz.wcovBy + isMaximal_inf_left_of_isMaximal_sup := inf_covBy_of_covBy_sup_of_covBy_sup_left Iso := Iso iso_symm := iso_symm iso_trans := iso_trans diff --git a/Mathlib/SetTheory/Ordinal/Topology.lean b/Mathlib/SetTheory/Ordinal/Topology.lean index e23eae9da1d32..863f9c240874c 100644 --- a/Mathlib/SetTheory/Ordinal/Topology.lean +++ b/Mathlib/SetTheory/Ordinal/Topology.lean @@ -54,7 +54,7 @@ theorem isOpen_singleton_iff : IsOpen ({a} : Set Ordinal) ↔ ¬IsLimit a := by #align ordinal.is_open_singleton_iff Ordinal.isOpen_singleton_iff -- porting note: todo: generalize to a `SuccOrder` -theorem nhds_right' (a : Ordinal) : 𝓝[>] a = ⊥ := (covby_succ a).nhdsWithin_Ioi +theorem nhds_right' (a : Ordinal) : 𝓝[>] a = ⊥ := (covBy_succ a).nhdsWithin_Ioi -- todo: generalize to a `SuccOrder` theorem nhds_left'_eq_nhds_ne (a : Ordinal) : 𝓝[<] a = 𝓝[≠] a := by diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean index 79e9ac3c22c72..1f61fbdcad17d 100644 --- a/Mathlib/Topology/Order/Basic.lean +++ b/Mathlib/Topology/Order/Basic.lean @@ -414,7 +414,7 @@ theorem Ioo_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioo a c ∈ theorem Ioo_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Ioo a b ∈ 𝓝[>] a := Ioo_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩ -theorem Covby.nhdsWithin_Ioi {a b : α} (h : a ⋖ b) : 𝓝[>] a = ⊥ := +theorem CovBy.nhdsWithin_Ioi {a b : α} (h : a ⋖ b) : 𝓝[>] a = ⊥ := empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsWithin_Ioi' h.1 theorem Ioc_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioc a c ∈ 𝓝[>] b := @@ -476,7 +476,7 @@ theorem Ioo_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Ioo a c ∈ theorem Ioo_mem_nhdsWithin_Iio' {a b : α} (H : a < b) : Ioo a b ∈ 𝓝[<] b := Ioo_mem_nhdsWithin_Iio ⟨H, le_rfl⟩ -theorem Covby.nhdsWithin_Iio {a b : α} (h : a ⋖ b) : 𝓝[<] b = ⊥ := +theorem CovBy.nhdsWithin_Iio {a b : α} (h : a ⋖ b) : 𝓝[<] b = ⊥ := empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsWithin_Iio' h.1 theorem Ico_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Ico a c ∈ 𝓝[<] b := @@ -1337,7 +1337,7 @@ variable {α} -- porting note: new lemma /-- The set of points which are isolated on the right is countable when the space is second-countable. -/ -theorem countable_setOf_covby_right [SecondCountableTopology α] : +theorem countable_setOf_covBy_right [SecondCountableTopology α] : Set.Countable { x : α | ∃ y, x ⋖ y } := by nontriviality α let s := { x : α | ∃ y, x ⋖ y } @@ -1379,24 +1379,24 @@ theorem countable_setOf_covby_right [SecondCountableTopology α] : /-- The set of points which are isolated on the right is countable when the space is second-countable. -/ -@[deprecated countable_setOf_covby_right] +@[deprecated countable_setOf_covBy_right] theorem countable_of_isolated_right' [SecondCountableTopology α] : Set.Countable { x : α | ∃ y, x < y ∧ Ioo x y = ∅ } := by - simpa only [← covby_iff_Ioo_eq] using countable_setOf_covby_right + simpa only [← covBy_iff_Ioo_eq] using countable_setOf_covBy_right #align countable_of_isolated_right countable_of_isolated_right' /-- The set of points which are isolated on the left is countable when the space is second-countable. -/ -theorem countable_setOf_covby_left [SecondCountableTopology α] : +theorem countable_setOf_covBy_left [SecondCountableTopology α] : Set.Countable { x : α | ∃ y, y ⋖ x } := by - convert countable_setOf_covby_right (α := αᵒᵈ) using 5 - exact toDual_covby_toDual_iff.symm + convert countable_setOf_covBy_right (α := αᵒᵈ) using 5 + exact toDual_covBy_toDual_iff.symm /-- The set of points which are isolated on the left is countable when the space is second-countable. -/ theorem countable_of_isolated_left' [SecondCountableTopology α] : Set.Countable { x : α | ∃ y, y < x ∧ Ioo y x = ∅ } := by - simpa only [← covby_iff_Ioo_eq] using countable_setOf_covby_left + simpa only [← covBy_iff_Ioo_eq] using countable_setOf_covBy_left #align countable_of_isolated_left countable_of_isolated_left' /-- Consider a disjoint family of intervals `(x, y)` with `x < y` in a second-countable space. @@ -1408,7 +1408,7 @@ theorem Set.PairwiseDisjoint.countable_of_Ioo [SecondCountableTopology α] {y : have : (s \ { x | ∃ y, x ⋖ y }).Countable := (h.subset (diff_subset _ _)).countable_of_isOpen (fun _ _ => isOpen_Ioo) fun x hx => (h' _ hx.1).exists_lt_lt (mt (Exists.intro (y x)) hx.2) - this.of_diff countable_setOf_covby_right + this.of_diff countable_setOf_covBy_right #align set.pairwise_disjoint.countable_of_Ioo Set.PairwiseDisjoint.countable_of_Ioo /-- For a function taking values in a second countable space, the set of points `x` for @@ -1689,7 +1689,7 @@ theorem nhdsWithin_Ioi_eq_bot_iff {a : α} : 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ · simp [ha, ha.isMax.Ioi_eq] · simp only [ha, false_or] rw [isTop_iff_isMax, not_isMax_iff] at ha - simp only [(nhdsWithin_Ioi_basis' ha).eq_bot_iff, covby_iff_Ioo_eq] + simp only [(nhdsWithin_Ioi_basis' ha).eq_bot_iff, covBy_iff_Ioo_eq] /-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)` with `a < u`. -/ @@ -1704,7 +1704,7 @@ second-countable. -/ theorem countable_setOf_isolated_right [SecondCountableTopology α] : { x : α | 𝓝[>] x = ⊥ }.Countable := by simp only [nhdsWithin_Ioi_eq_bot_iff, setOf_or] - exact (subsingleton_isTop α).countable.union countable_setOf_covby_right + exact (subsingleton_isTop α).countable.union countable_setOf_covBy_right /-- The set of points which are isolated on the left is countable when the space is second-countable. -/ @@ -1778,7 +1778,7 @@ theorem nhdsWithin_Iio_basis' {a : α} (h : ∃ b, b < a) : (𝓝[<] a).HasBasis theorem nhdsWithin_Iio_eq_bot_iff {a : α} : 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a := by convert (config := {preTransparency := .default}) nhdsWithin_Ioi_eq_bot_iff (a := OrderDual.toDual a) using 4 - exact ofDual_covby_ofDual_iff + exact ofDual_covBy_ofDual_iff open List in /-- The following statements are equivalent: diff --git a/Mathlib/Topology/Support.lean b/Mathlib/Topology/Support.lean index 238c5bc0e8d80..097fe3908338a 100644 --- a/Mathlib/Topology/Support.lean +++ b/Mathlib/Topology/Support.lean @@ -81,7 +81,7 @@ theorem range_subset_insert_image_mulTSupport (f : X → α) : @[to_additive] theorem range_eq_image_mulTSupport_or (f : X → α) : range f = f '' mulTSupport f ∨ range f = insert 1 (f '' mulTSupport f) := - (wcovby_insert _ _).eq_or_eq (image_subset_range _ _) (range_subset_insert_image_mulTSupport f) + (wcovBy_insert _ _).eq_or_eq (image_subset_range _ _) (range_subset_insert_image_mulTSupport f) #align range_eq_image_mul_tsupport_or range_eq_image_mulTSupport_or #align range_eq_image_tsupport_or range_eq_image_tsupport_or