deprecated aliases

Mathlib/Algebra/DirectSum/Module.lean

@@ -322,6 +322,9 @@ theorem IsInternal.submodule_iSup_eq_top (h : IsInternal A) : iSup A = ⊤ := by
 theorem IsInternal.submodule_iSupIndep (h : IsInternal A) : iSupIndep A :=
   iSupIndep_of_dfinsupp_lsum_injective _ h.injective
 
+@[deprecated (since := "2024-11-24")]
+alias IsInternal.submodule_independent := IsInternal.submodule_iSupIndep
+
 /-- Given an internal direct sum decomposition of a module `M`, and a basis for each of the
 components of the direct sum, the disjoint union of these bases is a basis for `M`. -/
 noncomputable def IsInternal.collectedBasis (h : IsInternal A) {α : ι → Type*}
@@ -395,13 +398,21 @@ theorem isInternal_submodule_of_iSupIndep_of_iSup_eq_top {A : ι → Submodule R
     (LinearMap.range_eq_top (f := DFinsupp.lsum _ _)).1 <|
       (Submodule.iSup_eq_range_dfinsupp_lsum _).symm.trans hs⟩
 
+@[deprecated (since := "2024-11-24")]
+alias isInternal_submodule_of_independent_of_iSup_eq_top :=
+  isInternal_submodule_of_iSupIndep_of_iSup_eq_top
+
 /-- `iff` version of `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top`,
 `DirectSum.IsInternal.iSupIndep`, and `DirectSum.IsInternal.submodule_iSup_eq_top`. -/
 theorem isInternal_submodule_iff_iSupIndep_and_iSup_eq_top (A : ι → Submodule R M) :
     IsInternal A ↔ iSupIndep A ∧ iSup A = ⊤ :=
   ⟨fun i ↦ ⟨i.submodule_iSupIndep, i.submodule_iSup_eq_top⟩,
     And.rec isInternal_submodule_of_iSupIndep_of_iSup_eq_top⟩
 
+@[deprecated (since := "2024-11-24")]
+alias isInternal_submodule_iff_independent_and_iSup_eq_top :=
+  isInternal_submodule_iff_iSupIndep_and_iSup_eq_top
+
 /-- If a collection of submodules has just two indices, `i` and `j`, then
 `DirectSum.IsInternal` is equivalent to `isCompl`. -/
 theorem isInternal_submodule_iff_isCompl (A : ι → Submodule R M) {i j : ι} (hij : i ≠ j)
@@ -430,17 +441,26 @@ lemma isInternal_biSup_submodule_of_iSupIndep {A : ι → Submodule R M} (s : Se
   change m ∈ ((A i).comap p.subtype).map p.subtype ↔ _
   rw [Submodule.map_comap_subtype, inf_of_le_right (hp i i.property)]
 
+@[deprecated (since := "2024-11-24")]
+alias isInternal_biSup_submodule_of_independent := isInternal_biSup_submodule_of_iSupIndep
+
 /-! Now copy the lemmas for subgroup and submonoids. -/
 
 
 theorem IsInternal.addSubmonoid_iSupIndep {M : Type*} [AddCommMonoid M] {A : ι → AddSubmonoid M}
     (h : IsInternal A) : iSupIndep A :=
   iSupIndep_of_dfinsupp_sumAddHom_injective _ h.injective
 
+@[deprecated (since := "2024-11-24")]
+alias IsInternal.addSubmonoid_independent := IsInternal.addSubmonoid_iSupIndep
+
 theorem IsInternal.addSubgroup_iSupIndep {G : Type*} [AddCommGroup G] {A : ι → AddSubgroup G}
     (h : IsInternal A) : iSupIndep A :=
   iSupIndep_of_dfinsupp_sumAddHom_injective' _ h.injective
 
+@[deprecated (since := "2024-11-24")]
+alias IsInternal.addSubgroup_independent := IsInternal.addSubgroup_iSupIndep
+
 end Ring
 
 end Submodule

Mathlib/Algebra/Lie/Submodule.lean

@@ -518,6 +518,9 @@ theorem iSupIndep_iff_coe_toSubmodule {ι : Type*} {N : ι → LieSubmodule R L
     iSupIndep N ↔ iSupIndep fun i ↦ (N i : Submodule R M) := by
   simp [iSupIndep_def, disjoint_iff_coe_toSubmodule]
 
+@[deprecated (since := "2024-11-24")]
+alias independent_iff_coe_toSubmodule := iSupIndep_iff_coe_toSubmodule
+
 theorem iSup_eq_top_iff_coe_toSubmodule {ι : Sort*} {N : ι → LieSubmodule R L M} :
     ⨆ i, N i = ⊤ ↔ ⨆ i, (N i : Submodule R M) = ⊤ := by
   rw [← iSup_coe_toSubmodule, ← top_coeSubmodule (L := L), coe_toSubmodule_eq_iff]

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -674,17 +674,24 @@ lemma iSupIndep_genWeightSpace [NoZeroSMulDivisors R M] :
   exact Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo (toEnd R L M)
     (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem)
 
+@[deprecated (since := "2024-11-24")] alias independent_genWeightSpace := iSupIndep_genWeightSpace
+
 lemma iSupIndep_genWeightSpace' [NoZeroSMulDivisors R M] :
     iSupIndep fun χ : Weight R L M ↦ genWeightSpace M χ :=
   (iSupIndep_genWeightSpace R L M).comp <|
     Subtype.val_injective.comp (Weight.equivSetOf R L M).injective
 
+@[deprecated (since := "2024-11-24")] alias independent_genWeightSpace' := iSupIndep_genWeightSpace'
+
 lemma iSupIndep_genWeightSpaceOf [NoZeroSMulDivisors R M] (x : L) :
     iSupIndep fun (χ : R) ↦ genWeightSpaceOf M χ x := by
   rw [LieSubmodule.iSupIndep_iff_coe_toSubmodule]
   dsimp [genWeightSpaceOf]
   exact (toEnd R L M x).independent_genEigenspace _
 
+@[deprecated (since := "2024-11-24")]
+alias independent_genWeightSpaceOf := iSupIndep_genWeightSpaceOf
+
 lemma finite_genWeightSpaceOf_ne_bot [NoZeroSMulDivisors R M] [IsNoetherian R M] (x : L) :
     {χ : R | genWeightSpaceOf M χ x ≠ ⊥}.Finite :=
   WellFoundedGT.finite_ne_bot_of_iSupIndep (iSupIndep_genWeightSpaceOf R L M x)

Mathlib/Algebra/Module/Torsion.lean

@@ -113,6 +113,9 @@ theorem iSupIndep.linearIndependent' {ι R M : Type*} {v : ι → M} [Ring R]
   rw [← Submodule.mem_bot R, ← h_ne_zero i]
   simpa using this
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.Independent.linear_independent' := iSupIndep.linearIndependent'
+
 end TorsionOf
 
 section

Mathlib/GroupTheory/NoncommPiCoprod.lean

@@ -73,6 +73,9 @@ theorem eq_one_of_noncommProd_eq_one_of_iSupIndep {ι : Type*} (s : Finset ι) (
       · exact heq1i
       · refine ih hcomm hmem.2 heq1S _ h
 
+@[deprecated (since := "2024-11-24")]
+alias eq_one_of_noncommProd_eq_one_of_independent := eq_one_of_noncommProd_eq_one_of_iSupIndep
+
 end Subgroup
 
 section FamilyOfMonoids
@@ -215,6 +218,9 @@ theorem injective_noncommPiCoprod_of_iSupIndep [Fintype ι]
     apply hinj
     simp [this i (Finset.mem_univ i)]
 
+@[deprecated (since := "2024-11-24")]
+alias injective_noncommPiCoprod_of_independent := injective_noncommPiCoprod_of_iSupIndep
+
 @[to_additive]
 theorem independent_range_of_coprime_order
     (hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y))

Mathlib/LinearAlgebra/DFinsupp.lean

@@ -410,6 +410,9 @@ theorem iSupIndep_iff_forall_dfinsupp (p : ι → Submodule R N) :
   refine forall_congr' fun i => Subtype.forall'.trans ?_
   simp_rw [Submodule.coe_eq_zero]
 
+@[deprecated (since := "2024-11-24")]
+alias independent_iff_forall_dfinsupp := iSupIndep_iff_forall_dfinsupp
+
 /- If `DFinsupp.lsum` applied with `Submodule.subtype` is injective then the submodules are
 iSupIndep. -/
 theorem iSupIndep_of_dfinsupp_lsum_injective (p : ι → Submodule R N)
@@ -423,13 +426,19 @@ theorem iSupIndep_of_dfinsupp_lsum_injective (p : ι → Submodule R N)
   have := DFunLike.ext_iff.mp (h hv) i
   simpa [eq_comm] using this
 
+@[deprecated (since := "2024-11-24")]
+alias independent_of_dfinsupp_lsum_injective := iSupIndep_of_dfinsupp_lsum_injective
+
 /- If `DFinsupp.sumAddHom` applied with `AddSubmonoid.subtype` is injective then the additive
 submonoids are independent. -/
 theorem iSupIndep_of_dfinsupp_sumAddHom_injective (p : ι → AddSubmonoid N)
     (h : Function.Injective (sumAddHom fun i => (p i).subtype)) : iSupIndep p := by
   rw [← iSupIndep_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoid N ≃o _)]
   exact iSupIndep_of_dfinsupp_lsum_injective _ h
 
+@[deprecated (since := "2024-11-24")]
+alias independent_of_dfinsupp_sumAddHom_injective := iSupIndep_of_dfinsupp_sumAddHom_injective
+
 /-- Combining `DFinsupp.lsum` with `LinearMap.toSpanSingleton` is the same as
 `Finsupp.linearCombination` -/
 theorem lsum_comp_mapRange_toSpanSingleton [∀ m : R, Decidable (m ≠ 0)] (p : ι → Submodule R N)
@@ -455,6 +464,9 @@ theorem iSupIndep_of_dfinsupp_sumAddHom_injective' (p : ι → AddSubgroup N)
   rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)]
   exact iSupIndep_of_dfinsupp_lsum_injective _ h
 
+@[deprecated (since := "2024-11-24")]
+alias independent_of_dfinsupp_sumAddHom_injective' := iSupIndep_of_dfinsupp_sumAddHom_injective'
+
 /-- The canonical map out of a direct sum of a family of submodules is injective when the submodules
 are `iSupIndep`.
 
@@ -480,13 +492,19 @@ theorem iSupIndep.dfinsupp_lsum_injective {p : ι → Submodule R N} (h : iSupIn
   rwa [← erase_add_single i m, LinearMap.map_add, lsum_single, Submodule.subtype_apply,
     add_eq_zero_iff_eq_neg, ← Submodule.coe_neg] at hm
 
+@[deprecated (since := "2024-11-24")]
+alias Independent.dfinsupp_lsum_injective := iSupIndep.dfinsupp_lsum_injective
+
 /-- The canonical map out of a direct sum of a family of additive subgroups is injective when the
 additive subgroups are `iSupIndep`. -/
 theorem iSupIndep.dfinsupp_sumAddHom_injective {p : ι → AddSubgroup N} (h : iSupIndep p) :
     Function.Injective (sumAddHom fun i => (p i).subtype) := by
   rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)] at h
   exact h.dfinsupp_lsum_injective
 
+@[deprecated (since := "2024-11-24")]
+alias Independent.dfinsupp_sumAddHom_injective := iSupIndep.dfinsupp_sumAddHom_injective
+
 /-- A family of submodules over an additive group are independent if and only iff `DFinsupp.lsum`
 applied with `Submodule.subtype` is injective.
 
@@ -496,12 +514,18 @@ theorem iSupIndep_iff_dfinsupp_lsum_injective (p : ι → Submodule R N) :
     iSupIndep p ↔ Function.Injective (lsum ℕ (M := fun i ↦ ↥(p i)) fun i => (p i).subtype) :=
   ⟨iSupIndep.dfinsupp_lsum_injective, iSupIndep_of_dfinsupp_lsum_injective p⟩
 
+@[deprecated (since := "2024-11-24")]
+alias independent_iff_dfinsupp_lsum_injective := iSupIndep_iff_dfinsupp_lsum_injective
+
 /-- A family of additive subgroups over an additive group are independent if and only if
 `DFinsupp.sumAddHom` applied with `AddSubgroup.subtype` is injective. -/
 theorem iSupIndep_iff_dfinsupp_sumAddHom_injective (p : ι → AddSubgroup N) :
     iSupIndep p ↔ Function.Injective (sumAddHom fun i => (p i).subtype) :=
   ⟨iSupIndep.dfinsupp_sumAddHom_injective, iSupIndep_of_dfinsupp_sumAddHom_injective' p⟩
 
+@[deprecated (since := "2024-11-24")]
+alias independent_iff_dfinsupp_sumAddHom_injective := iSupIndep_iff_dfinsupp_sumAddHom_injective
+
 /-- If a family of submodules is independent, then a choice of nonzero vector from each submodule
 forms a linearly independent family.
 
@@ -525,12 +549,18 @@ theorem iSupIndep.linearIndependent [NoZeroSMulDivisors R N] {ι} (p : ι → Su
   simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
   simpa
 
+@[deprecated (since := "2024-11-24")]
+alias Independent.linearIndependent := iSupIndep.linearIndependent
+
 theorem iSupIndep_iff_linearIndependent_of_ne_zero [NoZeroSMulDivisors R N] {ι} {v : ι → N}
     (h_ne_zero : ∀ i, v i ≠ 0) : (iSupIndep fun i => R ∙ v i) ↔ LinearIndependent R v :=
   let _ := Classical.decEq ι
   ⟨fun hv => hv.linearIndependent _ (fun i => Submodule.mem_span_singleton_self <| v i) h_ne_zero,
     fun hv => hv.iSupIndep_span_singleton⟩
 
+@[deprecated (since := "2024-11-24")]
+alias independent_iff_linearIndependent_of_ne_zero := iSupIndep_iff_linearIndependent_of_ne_zero
+
 end Ring
 
 namespace LinearMap

Mathlib/LinearAlgebra/Dimension/Finite.lean

@@ -261,6 +261,9 @@ theorem iSupIndep.subtype_ne_bot_le_rank [Nontrivial R]
   have : LinearIndependent R v := (hV.comp Subtype.coe_injective).linearIndependent _ hvV hv
   exact this.cardinal_lift_le_rank
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.Independent.subtype_ne_bot_le_rank := iSupIndep.subtype_ne_bot_le_rank
+
 variable [Module.Finite R M] [StrongRankCondition R]
 
 theorem iSupIndep.subtype_ne_bot_le_finrank_aux

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -718,6 +718,8 @@ theorem eigenspaces_iSupIndep [NoZeroSMulDivisors R M] (f : End R M) :
     iSupIndep f.eigenspace :=
   (f.independent_genEigenspace 1).mono fun _ ↦ le_rfl
 
+@[deprecated (since := "2024-11-24")] alias eigenspaces_independent := eigenspaces_iSupIndep
+
 /-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly
     independent. -/
 theorem eigenvectors_linearIndependent' {ι : Type*} [NoZeroSMulDivisors R M]

Mathlib/LinearAlgebra/LinearIndependent.lean

@@ -928,6 +928,9 @@ theorem LinearIndependent.iSupIndep_span_singleton (hv : LinearIndependent R v)
   ext
   simp
 
+@[deprecated (since := "2024-11-24")]
+alias LinearIndependent.independent_span_singleton := LinearIndependent.iSupIndep_span_singleton
+
 variable (R)
 
 theorem exists_maximal_independent' (s : ι → M) :

Mathlib/LinearAlgebra/Projectivization/Independence.lean

@@ -66,6 +66,9 @@ theorem independent_iff_iSupIndep : Independent f ↔ iSupIndep fun i => (f i).s
     · simpa only [Function.comp_apply, submodule_eq] using Submodule.mem_span_singleton_self _
     · exact rep_nonzero (f i)
 
+@[deprecated (since := "2024-11-24")]
+alias independent_iff_completeLattice_independent := independent_iff_iSupIndep
+
 /-- A linearly dependent family of nonzero vectors gives a dependent family of points
 in projective space. -/
 inductive Dependent : (ι → ℙ K V) → Prop

Mathlib/Order/CompactlyGenerated/Basic.lean

@@ -293,16 +293,26 @@ theorem WellFoundedGT.finite_of_sSupIndep [WellFoundedGT α] {s : Set α}
     rw [← hs, eq_comm, inf_eq_left]
     exact le_sSup hx₀
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.WellFoundedGT.finite_of_setIndependent := WellFoundedGT.finite_of_sSupIndep
+
 theorem WellFoundedGT.finite_ne_bot_of_iSupIndep [WellFoundedGT α]
     {ι : Type*} {t : ι → α} (ht : iSupIndep t) : Set.Finite {i | t i ≠ ⊥} := by
   refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn
   exact WellFoundedGT.finite_of_sSupIndep ht.sSupIndep_range
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent :=
+  WellFoundedGT.finite_ne_bot_of_iSupIndep
+
 theorem WellFoundedGT.finite_of_iSupIndep [WellFoundedGT α] {ι : Type*}
     {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Finite ι :=
   haveI := (WellFoundedGT.finite_of_sSupIndep ht.sSupIndep_range).to_subtype
   Finite.of_injective_finite_range (ht.injective h_ne_bot)
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.WellFoundedGT.finite_of_independent := WellFoundedGT.finite_of_iSupIndep
+
 theorem WellFoundedLT.finite_of_sSupIndep [WellFoundedLT α] {s : Set α}
     (hs : sSupIndep s) : s.Finite := by
   by_contra inf
@@ -315,16 +325,26 @@ theorem WellFoundedLT.finite_of_sSupIndep [WellFoundedLT α] {s : Set α}
   · exact (RelEmbedding.natGT a lt).not_wellFounded_of_decreasing_seq wellFounded_lt
   exact ⟨(e i).2.1, fun h ↦ n.lt_succ_self.not_le <| hi.trans_eq <| e.2 <| Subtype.val_injective h⟩
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.WellFoundedLT.finite_of_setIndependent := WellFoundedLT.finite_of_sSupIndep
+
 theorem WellFoundedLT.finite_ne_bot_of_iSupIndep [WellFoundedLT α]
     {ι : Type*} {t : ι → α} (ht : iSupIndep t) : Set.Finite {i | t i ≠ ⊥} := by
   refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn
   exact WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.WellFoundedLT.finite_ne_bot_of_independent :=
+  WellFoundedLT.finite_ne_bot_of_iSupIndep
+
 theorem WellFoundedLT.finite_of_iSupIndep [WellFoundedLT α] {ι : Type*}
     {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Finite ι :=
   haveI := (WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range).to_subtype
   Finite.of_injective_finite_range (ht.injective h_ne_bot)
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.WellFoundedLT.finite_of_independent := WellFoundedLT.finite_of_iSupIndep
+
 /-- A complete lattice is said to be compactly generated if any
 element is the `sSup` of compact elements. -/
 class IsCompactlyGenerated (α : Type*) [CompleteLattice α] : Prop where
@@ -427,6 +447,9 @@ theorem sSupIndep_iff_finite {s : Set α} :
       · rw [Finset.coe_insert, Set.insert_subset_iff]
         exact ⟨ha, Set.Subset.trans ht diff_subset⟩⟩
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.setIndependent_iff_finite := sSupIndep_iff_finite
+
 lemma iSupIndep_iff_supIndep_of_injOn {ι : Type*} {f : ι → α}
     (hf : InjOn f {i | f i ≠ ⊥}) :
     iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f := by
@@ -450,6 +473,9 @@ lemma iSupIndep_iff_supIndep_of_injOn {ι : Type*} {f : ι → α}
   rw [Finset.supIndep_iff_disjoint_erase] at h
   exact h i (Finset.mem_insert_self i _)
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.independent_iff_supIndep_of_injOn := iSupIndep_iff_supIndep_of_injOn
+
 theorem sSupIndep_iUnion_of_directed {η : Type*} {s : η → Set α}
     (hs : Directed (· ⊆ ·) s) (h : ∀ i, sSupIndep (s i)) :
     sSupIndep (⋃ i, s i) := by
@@ -464,11 +490,17 @@ theorem sSupIndep_iUnion_of_directed {η : Type*} {s : η → Set α}
     exfalso
     exact hη ⟨i⟩
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.setIndependent_iUnion_of_directed := sSupIndep_iUnion_of_directed
+
 theorem iSupIndep_sUnion_of_directed {s : Set (Set α)} (hs : DirectedOn (· ⊆ ·) s)
     (h : ∀ a ∈ s, sSupIndep a) : sSupIndep (⋃₀ s) := by
   rw [Set.sUnion_eq_iUnion]
   exact sSupIndep_iUnion_of_directed hs.directed_val (by simpa using h)
 
+@[deprecated (since := "2024-11-24")]
+alias CompleteLattice.independent_sUnion_of_directed := iSupIndep_sUnion_of_directed
+
 end
 
 namespace CompleteLattice
@@ -496,7 +528,7 @@ alias _root_.WellFounded.isSupClosedCompact := WellFoundedGT.isSupClosedCompact
 @[deprecated (since := "2024-10-07")]
 alias WellFounded.finite_of_setIndependent := WellFoundedGT.finite_of_sSupIndep
 @[deprecated (since := "2024-10-07")]
-alias WellFounded.finite_ne_bot_of_iSupIndep := WellFoundedGT.finite_ne_bot_of_iSupIndep
+alias WellFounded.finite_ne_bot_of_independent := WellFoundedGT.finite_ne_bot_of_iSupIndep
 @[deprecated (since := "2024-10-07")]
 alias WellFounded.finite_of_independent := WellFoundedGT.finite_of_iSupIndep
 @[deprecated (since := "2024-10-07")]
@@ -632,11 +664,17 @@ theorem exists_sSupIndep_isCompl_sSup_atoms (h : sSup { a : α | IsAtom a } = 
     · exact s_atoms x hx
     · exact ha
 
+@[deprecated (since := "2024-11-24")]
+alias exists_setIndependent_isCompl_sSup_atoms := exists_sSupIndep_isCompl_sSup_atoms
+
 theorem exists_sSupIndep_of_sSup_atoms_eq_top (h : sSup { a : α | IsAtom a } = ⊤) :
     ∃ s : Set α, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a :=
   let ⟨s, s_ind, s_top, s_atoms⟩ := exists_sSupIndep_isCompl_sSup_atoms h ⊥
   ⟨s, s_ind, eq_top_of_isCompl_bot s_top.symm, s_atoms⟩
 
+@[deprecated (since := "2024-11-24")]
+alias exists_setIndependent_of_sSup_atoms_eq_top := exists_sSupIndep_of_sSup_atoms_eq_top
+
 /-- See [Theorem 6.6][calugareanu]. -/
 theorem complementedLattice_of_sSup_atoms_eq_top (h : sSup { a : α | IsAtom a } = ⊤) :
     ComplementedLattice α :=