Commit 2023-05-14 07:05 d1eb6264

View on Github →

chore: Rename to sSup/iSup (#3938) As discussed on Zulip

Renames

  • supₛ → sSup
  • infₛ → sInf
  • supᵢ → iSup
  • infᵢ → iInf
  • bsupₛ → bsSup
  • binfₛ → bsInf
  • bsupᵢ → biSup
  • binfᵢ → biInf
  • csupₛ → csSup
  • cinfₛ → csInf
  • csupᵢ → ciSup
  • cinfᵢ → ciInf
  • unionₛ → sUnion
  • interₛ → sInter
  • unionᵢ → iUnion
  • interᵢ → iInter
  • bunionₛ → bsUnion
  • binterₛ → bsInter
  • bunionᵢ → biUnion
  • binterᵢ → biInter

Estimated changes

added theorem Submodule.iSup_mul
added theorem Submodule.mul_iSup
deleted theorem Submodule.mul_supᵢ
deleted theorem Submodule.supᵢ_mul
added theorem Algebra.coe_iInf
deleted theorem Algebra.coe_infᵢ
deleted theorem Algebra.coe_infₛ
added theorem Algebra.coe_sInf
added theorem Algebra.mem_iInf
deleted theorem Algebra.mem_infᵢ
deleted theorem Algebra.mem_infₛ
added theorem Algebra.mem_sInf
added theorem Subalgebra.iSupLift_mk
deleted theorem Subalgebra.supᵢLift_mk
added theorem Finset.card_biUnion
added theorem Finset.card_biUnion_le
deleted theorem Finset.card_bunionᵢ
deleted theorem Finset.card_bunionᵢ_le
deleted theorem Finset.card_disjUnionᵢ
added theorem Finset.card_disjiUnion
added theorem Finset.prod_biUnion
deleted theorem Finset.prod_bunionᵢ
deleted theorem Finset.prod_disjUnionᵢ
added theorem Finset.prod_disjiUnion
added theorem finprod_mem_biUnion
deleted theorem finprod_mem_bunionᵢ
added theorem finprod_mem_iUnion
added theorem finprod_mem_sUnion
deleted theorem finprod_mem_unionᵢ
deleted theorem finprod_mem_unionₛ
added theorem ciSup_div
added theorem ciSup_mul
deleted theorem csupᵢ_div
deleted theorem csupᵢ_mul
added theorem mul_ciSup
deleted theorem mul_csupᵢ
deleted theorem LieSubalgebra.infₛ_coe
deleted theorem LieSubalgebra.infₛ_glb
added theorem LieSubalgebra.sInf_coe
added theorem LieSubalgebra.sInf_glb
added theorem Submodule.iInf_coe
deleted theorem Submodule.infᵢ_coe
deleted theorem Submodule.infₛ_coe
added theorem Submodule.mem_iInf
deleted theorem Submodule.mem_infᵢ
deleted theorem Submodule.mem_infₛ
added theorem Submodule.mem_sInf
added theorem Submodule.sInf_coe
deleted theorem Submodule.sum_mem_bsupᵢ
added theorem Submodule.sum_mem_iSup
deleted theorem Submodule.sum_mem_supᵢ
added theorem Submodule.neg_iInf
added theorem Submodule.neg_iSup
deleted theorem Submodule.neg_infᵢ
deleted theorem Submodule.neg_supᵢ
deleted theorem cinfₛ_div
deleted theorem cinfₛ_inv
deleted theorem cinfₛ_mul
deleted theorem cinfₛ_one
added theorem csInf_div
added theorem csInf_inv
added theorem csInf_mul
added theorem csInf_one
added theorem csSup_div
added theorem csSup_inv
added theorem csSup_mul
added theorem csSup_one
deleted theorem csupₛ_div
deleted theorem csupₛ_inv
deleted theorem csupₛ_mul
deleted theorem csupₛ_one
deleted theorem infₛ_div
deleted theorem infₛ_inv
deleted theorem infₛ_mul
deleted theorem infₛ_one
added theorem sInf_div
added theorem sInf_inv
added theorem sInf_mul
added theorem sInf_one
added theorem sSup_div
added theorem sSup_inv
added theorem sSup_mul
added theorem sSup_one
deleted theorem supₛ_div
deleted theorem supₛ_inv
deleted theorem supₛ_mul
deleted theorem supₛ_one
added theorem iUnion_Icc_add_zsmul
added theorem iUnion_Icc_int_cast
added theorem iUnion_Icc_zsmul
added theorem iUnion_Ico_add_zsmul
added theorem iUnion_Ico_int_cast
added theorem iUnion_Ico_zsmul
added theorem iUnion_Ioc_add_zsmul
added theorem iUnion_Ioc_int_cast
added theorem iUnion_Ioc_zsmul
deleted theorem unionᵢ_Icc_add_int_cast
deleted theorem unionᵢ_Icc_add_zsmul
deleted theorem unionᵢ_Icc_int_cast
deleted theorem unionᵢ_Icc_zsmul
deleted theorem unionᵢ_Ico_add_int_cast
deleted theorem unionᵢ_Ico_add_zsmul
deleted theorem unionᵢ_Ico_int_cast
deleted theorem unionᵢ_Ico_zsmul
deleted theorem unionᵢ_Ioc_add_int_cast
deleted theorem unionᵢ_Ioc_add_zsmul
deleted theorem unionᵢ_Ioc_int_cast
deleted theorem unionᵢ_Ioc_zsmul
added theorem Set.iInter_star
added theorem Set.iUnion_star
deleted theorem Set.interᵢ_star
deleted theorem Set.unionᵢ_star
deleted theorem StarSubalgebra.coe_infᵢ
deleted theorem StarSubalgebra.coe_infₛ
deleted theorem StarSubalgebra.mem_infᵢ
deleted theorem StarSubalgebra.mem_infₛ
added theorem trop_iInf
deleted theorem trop_infᵢ
deleted theorem trop_infₛ_image
added theorem trop_sInf_image
added theorem Directed.convex_iUnion
deleted theorem Directed.convex_unionᵢ
added theorem convex_iInter
added theorem convex_iInter₂
deleted theorem convex_interᵢ
deleted theorem convex_interᵢ₂
deleted theorem convex_interₛ
added theorem convex_sInter
deleted theorem IsExposed.interₛ
added theorem IsExposed.sInter
added theorem isExtreme_biInter
deleted theorem isExtreme_binterᵢ
added theorem isExtreme_iInter
deleted theorem isExtreme_interᵢ
deleted theorem isExtreme_interₛ
added theorem isExtreme_sInter
modified theorem gauge_def'
modified theorem gauge_def
added theorem convexHull_eq_iInter
deleted theorem convexHull_eq_interᵢ
added theorem convexJoin_iUnion_left
deleted theorem convexJoin_unionᵢ_left
deleted theorem convexJoin_unionᵢ_right
added theorem starConvex_iInter
added theorem starConvex_iUnion
deleted theorem starConvex_interᵢ
deleted theorem starConvex_interₛ
added theorem starConvex_sInter
added theorem starConvex_sUnion
deleted theorem starConvex_unionᵢ
deleted theorem starConvex_unionₛ
added theorem balancedCore_eq_iInter
deleted theorem balancedCore_eq_interᵢ
added theorem absorbs_iUnion_finset
deleted theorem absorbs_unionᵢ_finset
added theorem balanced_iInter
added theorem balanced_iInter₂
added theorem balanced_iUnion
added theorem balanced_iUnion₂
deleted theorem balanced_interᵢ
deleted theorem balanced_interᵢ₂
deleted theorem balanced_unionᵢ
deleted theorem balanced_unionᵢ₂
added theorem LinearMap.polar_iUnion
deleted theorem LinearMap.polar_unionᵢ
modified theorem NormedAddGroupHom.norm_def
added theorem SimpleGraph.iInf_adj
added theorem SimpleGraph.iSup_adj
deleted theorem SimpleGraph.infᵢ_adj
deleted theorem SimpleGraph.infₛ_adj
added theorem SimpleGraph.sInf_adj
added theorem SimpleGraph.sSup_adj
deleted theorem SimpleGraph.supᵢ_adj
deleted theorem SimpleGraph.supₛ_adj
added theorem Rel.interedges_biUnion
deleted theorem Rel.interedges_bunionᵢ
added theorem Language.add_iSup
deleted theorem Language.add_supᵢ
added theorem Language.iSup_add
added theorem Language.iSup_mul
added theorem Language.mem_iSup
deleted theorem Language.mem_supᵢ
added theorem Language.mul_iSup
deleted theorem Language.mul_supᵢ
deleted theorem Language.supᵢ_add
deleted theorem Language.supᵢ_mul
added theorem ENat.coe_iSup
deleted theorem ENat.coe_supᵢ
added theorem ENat.iSup_coe_lt_top
deleted theorem ENat.supᵢ_coe_lt_top
deleted theorem Finset.Nonempty.bunionᵢ
added theorem Finset.biUnion_biUnion
added theorem Finset.biUnion_congr
added theorem Finset.biUnion_empty
added theorem Finset.biUnion_insert
added theorem Finset.biUnion_inter
added theorem Finset.biUnion_mono
added theorem Finset.biUnion_subset
added theorem Finset.biUnion_val
deleted theorem Finset.bunionᵢ_congr
deleted theorem Finset.bunionᵢ_empty
deleted theorem Finset.bunionᵢ_insert
deleted theorem Finset.bunionᵢ_inter
deleted theorem Finset.bunionᵢ_mono
deleted theorem Finset.bunionᵢ_nonempty
deleted theorem Finset.bunionᵢ_subset
deleted theorem Finset.bunionᵢ_val
added theorem Finset.coe_biUnion
deleted theorem Finset.coe_bunionᵢ
deleted theorem Finset.coe_disjUnionᵢ
added theorem Finset.coe_disjiUnion
deleted def Finset.disjUnionᵢ
deleted theorem Finset.disjUnionᵢ_cons
deleted theorem Finset.disjUnionᵢ_empty
deleted theorem Finset.disjUnionᵢ_val
added theorem Finset.disjiUnion_cons
added theorem Finset.disjiUnion_val
added theorem Finset.erase_biUnion
deleted theorem Finset.erase_bunionᵢ
added theorem Finset.filter_biUnion
deleted theorem Finset.filter_bunionᵢ
added theorem Finset.inter_biUnion
deleted theorem Finset.inter_bunionᵢ
added theorem Finset.mem_biUnion
deleted theorem Finset.mem_bunionᵢ
deleted theorem Finset.mem_disjUnionᵢ
added theorem Finset.mem_disjiUnion
deleted theorem Finset.fold_disjUnionᵢ
added theorem Finset.fold_disjiUnion
added theorem Finset.biUnion_image
deleted theorem Finset.bunionᵢ_image
deleted theorem Finset.disjUnionᵢ_map
added theorem Finset.disjiUnion_map
added theorem Finset.image_biUnion
deleted theorem Finset.image_bunionᵢ
deleted theorem Finset.map_disjUnionᵢ
added theorem Finset.map_disjiUnion
added theorem Finset.iInf_biUnion
added theorem Finset.iInf_coe
added theorem Finset.iInf_insert
added theorem Finset.iInf_singleton
added theorem Finset.iInf_union
added theorem Finset.iSup_biUnion
added theorem Finset.iSup_coe
added theorem Finset.iSup_insert
added theorem Finset.iSup_singleton
added theorem Finset.iSup_union
added theorem Finset.inf'_biUnion
deleted theorem Finset.inf'_bunionᵢ
added theorem Finset.inf_biUnion
deleted theorem Finset.inf_bunionᵢ
added theorem Finset.inf_eq_iInf
deleted theorem Finset.inf_eq_infᵢ
deleted theorem Finset.inf_id_eq_infₛ
added theorem Finset.inf_id_eq_sInf
deleted theorem Finset.infᵢ_bunionᵢ
deleted theorem Finset.infᵢ_coe
deleted theorem Finset.infᵢ_insert
deleted theorem Finset.infᵢ_singleton
deleted theorem Finset.infᵢ_union
added theorem Finset.set_biInter_coe
added theorem Finset.set_biUnion_coe
deleted theorem Finset.set_binterᵢ_coe
deleted theorem Finset.set_bunionᵢ_coe
added theorem Finset.sup'_biUnion
deleted theorem Finset.sup'_bunionᵢ
added theorem Finset.sup_biUnion
deleted theorem Finset.sup_bunionᵢ
added theorem Finset.sup_eq_biUnion
deleted theorem Finset.sup_eq_bunionᵢ
added theorem Finset.sup_eq_iSup
deleted theorem Finset.sup_eq_supᵢ
added theorem Finset.sup_id_eq_sSup
deleted theorem Finset.sup_id_eq_supₛ
deleted theorem Finset.supᵢ_bunionᵢ
deleted theorem Finset.supᵢ_coe
deleted theorem Finset.supᵢ_insert
deleted theorem Finset.supᵢ_singleton
deleted theorem Finset.supᵢ_union
added theorem iInf_eq_iInf_finset'
added theorem iInf_eq_iInf_finset
added theorem iSup_eq_iSup_finset'
added theorem iSup_eq_iSup_finset
deleted theorem infᵢ_eq_infᵢ_finset'
deleted theorem infᵢ_eq_infᵢ_finset
deleted theorem supᵢ_eq_supᵢ_finset'
deleted theorem supᵢ_eq_supᵢ_finset
added theorem Finset.product_biUnion
deleted theorem Finset.product_bunionᵢ
deleted theorem Finset.sigma_eq_bunionᵢ
added theorem Finset.biUnion_slice
deleted theorem Finset.bunionᵢ_slice
added theorem Set.sized_iUnion
added theorem Set.sized_iUnion₂
deleted theorem Set.sized_unionᵢ
deleted theorem Set.sized_unionᵢ₂
deleted theorem Finset.inf_univ_eq_infᵢ
deleted theorem Finset.sup_univ_eq_supᵢ
deleted theorem Int.cinfₛ_empty
deleted theorem Int.cinfₛ_mem
added theorem Int.csInf_empty
added theorem Int.csInf_mem
added theorem Int.csSup_empty
added theorem Int.csSup_mem
deleted theorem Int.csupₛ_empty
deleted theorem Int.csupₛ_mem
added theorem Nat.iInf_lt_succ'
added theorem Nat.iInf_lt_succ
added theorem Nat.iInf_of_empty
added theorem Nat.iSup_lt_succ'
added theorem Nat.iSup_lt_succ
deleted theorem Nat.infᵢ_lt_succ'
deleted theorem Nat.infᵢ_lt_succ
deleted theorem Nat.infᵢ_of_empty
deleted theorem Nat.infₛ_add'
deleted theorem Nat.infₛ_add
deleted theorem Nat.infₛ_def
deleted theorem Nat.infₛ_empty
deleted theorem Nat.infₛ_eq_zero
deleted theorem Nat.infₛ_mem
deleted theorem Nat.not_mem_of_lt_infₛ
added theorem Nat.not_mem_of_lt_sInf
added theorem Nat.sInf_add'
added theorem Nat.sInf_add
added theorem Nat.sInf_def
added theorem Nat.sInf_empty
added theorem Nat.sInf_eq_zero
added theorem Nat.sInf_mem
added theorem Nat.sSup_def
added theorem Nat.sSup_mem
deleted theorem Nat.supᵢ_lt_succ'
deleted theorem Nat.supᵢ_lt_succ
deleted theorem Nat.supₛ_def
deleted theorem Nat.supₛ_mem
added theorem Set.biInter_lt_succ'
added theorem Set.biInter_lt_succ
added theorem Set.biUnion_lt_succ'
added theorem Set.biUnion_lt_succ
deleted theorem Set.binterᵢ_lt_succ'
deleted theorem Set.binterᵢ_lt_succ
deleted theorem Set.bunionᵢ_lt_succ'
deleted theorem Set.bunionᵢ_lt_succ
added theorem Set.iInter_unpair
added theorem Set.iUnion_unpair
added theorem Set.iUnion_unpair_prod
deleted theorem Set.interᵢ_unpair
deleted theorem Set.unionᵢ_unpair
deleted theorem Set.unionᵢ_unpair_prod
added theorem iInf_unpair
added theorem iSup_unpair
deleted theorem infᵢ_unpair
deleted theorem supᵢ_unpair
added theorem Real.add_neg_lt_sSup
deleted theorem Real.add_neg_lt_supₛ
added theorem Real.ciInf_const_zero
added theorem Real.ciInf_empty
added theorem Real.ciSup_const_zero
added theorem Real.ciSup_empty
deleted theorem Real.cinfᵢ_const_zero
deleted theorem Real.cinfᵢ_empty
deleted theorem Real.csupᵢ_const_zero
deleted theorem Real.csupᵢ_empty
added theorem Real.iInf_nonneg
deleted theorem Real.infᵢ_nonneg
deleted theorem Real.infₛ_def
deleted theorem Real.infₛ_empty
deleted theorem Real.infₛ_le_iff
deleted theorem Real.infₛ_le_supₛ
deleted theorem Real.infₛ_nonneg
deleted theorem Real.infₛ_nonpos
added theorem Real.le_sSup_iff
deleted theorem Real.le_supₛ_iff
deleted theorem Real.lt_infₛ_add_pos
added theorem Real.lt_sInf_add_pos
added theorem Real.sInf_def
added theorem Real.sInf_empty
added theorem Real.sInf_le_iff
added theorem Real.sInf_le_sSup
added theorem Real.sInf_nonneg
added theorem Real.sInf_nonpos
added theorem Real.sSup_def
added theorem Real.sSup_empty
added theorem Real.sSup_nonneg
added theorem Real.sSup_nonpos
added theorem Real.sSup_univ
deleted theorem Real.supₛ_def
deleted theorem Real.supₛ_empty
deleted theorem Real.supₛ_nonneg
deleted theorem Real.supₛ_nonpos
deleted theorem Real.supₛ_univ
added theorem ENNReal.add_iInf
deleted theorem ENNReal.add_infᵢ
added theorem ENNReal.coe_iInf
deleted theorem ENNReal.coe_infᵢ
deleted theorem ENNReal.coe_infₛ
added theorem ENNReal.coe_sInf
added theorem ENNReal.coe_sSup
deleted theorem ENNReal.coe_supₛ
added theorem ENNReal.iInf_add
added theorem ENNReal.iInf_add_iInf
added theorem ENNReal.iInf_ennreal
added theorem ENNReal.iInf_mul
added theorem ENNReal.iInf_mul_of_ne
added theorem ENNReal.iInf_ne_top
added theorem ENNReal.iInf_sum
added theorem ENNReal.iSup_coe_nat
added theorem ENNReal.iSup_ennreal
added theorem ENNReal.iSup_eq_zero
added theorem ENNReal.iSup_ne_top
added theorem ENNReal.iSup_sub
deleted theorem ENNReal.infᵢ_add
deleted theorem ENNReal.infᵢ_add_infᵢ
deleted theorem ENNReal.infᵢ_ennreal
deleted theorem ENNReal.infᵢ_mul
deleted theorem ENNReal.infᵢ_mul_of_ne
deleted theorem ENNReal.infᵢ_ne_top
deleted theorem ENNReal.infᵢ_sum
deleted theorem ENNReal.infₛ_add
added theorem ENNReal.mul_iInf
added theorem ENNReal.mul_iInf_of_ne
deleted theorem ENNReal.mul_infᵢ
deleted theorem ENNReal.mul_infᵢ_of_ne
added theorem ENNReal.sInf_add
deleted theorem ENNReal.sub_eq_infₛ
added theorem ENNReal.sub_eq_sInf
added theorem ENNReal.sub_iInf
deleted theorem ENNReal.sub_infᵢ
deleted theorem ENNReal.supᵢ_coe_nat
deleted theorem ENNReal.supᵢ_ennreal
deleted theorem ENNReal.supᵢ_eq_zero
deleted theorem ENNReal.supᵢ_ne_top
deleted theorem ENNReal.supᵢ_sub
added theorem ENNReal.toNNReal_iInf
deleted theorem ENNReal.toNNReal_infᵢ
added theorem ENNReal.toReal_iInf
deleted theorem ENNReal.toReal_infᵢ
added theorem Hyperreal.isSt_sSup
deleted theorem Hyperreal.isSt_supₛ
added theorem Hyperreal.st_eq_sSup
deleted theorem Hyperreal.st_eq_supₛ
added theorem NNReal.coe_iInf
added theorem NNReal.coe_iSup
deleted theorem NNReal.coe_infᵢ
deleted theorem NNReal.coe_infₛ
added theorem NNReal.coe_sInf
added theorem NNReal.coe_sSup
deleted theorem NNReal.coe_supᵢ
deleted theorem NNReal.coe_supₛ
added theorem NNReal.iInf_const_zero
added theorem NNReal.iInf_empty
added theorem NNReal.iInf_mul
added theorem NNReal.iSup_div
added theorem NNReal.iSup_empty
added theorem NNReal.iSup_mul
added theorem NNReal.iSup_mul_le
deleted theorem NNReal.infᵢ_const_zero
deleted theorem NNReal.infᵢ_empty
deleted theorem NNReal.infᵢ_mul
deleted theorem NNReal.infₛ_empty
added theorem NNReal.le_iInf_mul
deleted theorem NNReal.le_infᵢ_mul
added theorem NNReal.le_mul_iInf
deleted theorem NNReal.le_mul_infᵢ
added theorem NNReal.mul_iInf
added theorem NNReal.mul_iSup
added theorem NNReal.mul_iSup_le
deleted theorem NNReal.mul_infᵢ
deleted theorem NNReal.mul_supᵢ
deleted theorem NNReal.mul_supᵢ_le
added theorem NNReal.sInf_empty
deleted theorem NNReal.supᵢ_div
deleted theorem NNReal.supᵢ_empty
deleted theorem NNReal.supᵢ_mul
deleted theorem NNReal.supᵢ_mul_le
deleted theorem Real.infᵢ_mul_of_nonneg
deleted theorem Real.infᵢ_mul_of_nonpos
deleted theorem Real.mul_infᵢ_of_nonneg
deleted theorem Real.mul_infᵢ_of_nonpos
deleted theorem Real.mul_supᵢ_of_nonneg
deleted theorem Real.mul_supᵢ_of_nonpos
deleted theorem Real.supᵢ_mul_of_nonneg
deleted theorem Real.supᵢ_mul_of_nonpos
added theorem Set.biUnion_accumulate
deleted theorem Set.bunionᵢ_accumulate
added theorem Set.iUnion_accumulate
modified theorem Set.subset_accumulate
deleted theorem Set.unionᵢ_accumulate
added theorem Set.countable_iUnion
deleted theorem Set.countable_unionᵢ
added theorem Set.Finite.biUnion'
added theorem Set.Finite.biUnion
deleted theorem Set.Finite.bunionᵢ'
deleted theorem Set.Finite.bunionᵢ
deleted theorem Set.Finite.interₛ
added theorem Set.Finite.sInter
added theorem Set.Finite.sUnion
deleted theorem Set.Finite.unionₛ
added theorem Set.finite_iUnion
deleted theorem Set.finite_unionᵢ
added theorem IsGLB.biUnion_Ioi_eq
deleted theorem IsGLB.bunionᵢ_Ioi_eq
added theorem IsGLB.iUnion_Ioi_eq
deleted theorem IsGLB.unionᵢ_Ioi_eq
added theorem IsLUB.biUnion_Iio_eq
deleted theorem IsLUB.bunionᵢ_Iio_eq
added theorem IsLUB.iUnion_Iio_eq
deleted theorem IsLUB.unionᵢ_Iio_eq
added theorem Set.iUnion_Icc_left
added theorem Set.iUnion_Icc_right
added theorem Set.iUnion_Ici
added theorem Set.iUnion_Ico_left
added theorem Set.iUnion_Ico_right
added theorem Set.iUnion_Iic
added theorem Set.iUnion_Iio
added theorem Set.iUnion_Ioc_left
added theorem Set.iUnion_Ioc_right
added theorem Set.iUnion_Ioi
added theorem Set.iUnion_Ioo_left
added theorem Set.iUnion_Ioo_right
deleted theorem Set.unionᵢ_Icc_left
deleted theorem Set.unionᵢ_Icc_right
deleted theorem Set.unionᵢ_Ici
deleted theorem Set.unionᵢ_Ico_left
deleted theorem Set.unionᵢ_Ico_right
deleted theorem Set.unionᵢ_Iic
deleted theorem Set.unionᵢ_Iio
deleted theorem Set.unionᵢ_Ioc_left
deleted theorem Set.unionᵢ_Ioc_right
deleted theorem Set.unionᵢ_Ioi
deleted theorem Set.unionᵢ_Ioo_left
deleted theorem Set.unionᵢ_Ioo_right
added theorem iUnion_Ici_eq_Ici_iInf
added theorem iUnion_Ici_eq_Ioi_iInf
added theorem iUnion_Iic_eq_Iic_iSup
added theorem iUnion_Iic_eq_Iio_iSup
deleted theorem Set.ordConnected_interᵢ
deleted theorem Set.ordConnected_interₛ
deleted theorem Antitone.interᵢ_nat_add
deleted theorem Monotone.unionᵢ_nat_add
added theorem Set.Ici_iSup
added theorem Set.Ici_iSup₂
added theorem Set.Ici_sSup
deleted theorem Set.Ici_supᵢ
deleted theorem Set.Ici_supᵢ₂
deleted theorem Set.Ici_supₛ
added theorem Set.Iic_iInf
added theorem Set.Iic_iInf₂
deleted theorem Set.Iic_infᵢ
deleted theorem Set.Iic_infᵢ₂
deleted theorem Set.Iic_infₛ
added theorem Set.Iic_sInf
added theorem Set.Nonempty.of_sUnion
deleted theorem Set.Nonempty.of_unionₛ
added theorem Set.biInter_and'
added theorem Set.biInter_and
added theorem Set.biInter_empty
added theorem Set.biInter_eq_iInter
added theorem Set.biInter_iUnion
added theorem Set.biInter_image
added theorem Set.biInter_insert
added theorem Set.biInter_inter
added theorem Set.biInter_mono
added theorem Set.biInter_pair
added theorem Set.biInter_range
added theorem Set.biInter_singleton
added theorem Set.biInter_union
added theorem Set.biInter_univ
added theorem Set.biUnion_and'
added theorem Set.biUnion_and
added theorem Set.biUnion_empty
added theorem Set.biUnion_eq_iUnion
added theorem Set.biUnion_iUnion
added theorem Set.biUnion_image
added theorem Set.biUnion_insert
added theorem Set.biUnion_mono
added theorem Set.biUnion_pair
added theorem Set.biUnion_range
added theorem Set.biUnion_self
added theorem Set.biUnion_singleton
added theorem Set.biUnion_union
added theorem Set.biUnion_univ
added theorem Set.bijOn_iInter
added theorem Set.bijOn_iUnion
deleted theorem Set.bijOn_interᵢ
deleted theorem Set.bijOn_unionᵢ
deleted theorem Set.binterᵢ_and'
deleted theorem Set.binterᵢ_and
deleted theorem Set.binterᵢ_empty
deleted theorem Set.binterᵢ_eq_interᵢ
deleted theorem Set.binterᵢ_image
deleted theorem Set.binterᵢ_insert
deleted theorem Set.binterᵢ_inter
deleted theorem Set.binterᵢ_mono
deleted theorem Set.binterᵢ_pair
deleted theorem Set.binterᵢ_range
deleted theorem Set.binterᵢ_singleton
deleted theorem Set.binterᵢ_union
deleted theorem Set.binterᵢ_unionᵢ
deleted theorem Set.binterᵢ_univ
deleted theorem Set.bunionᵢ_and'
deleted theorem Set.bunionᵢ_and
deleted theorem Set.bunionᵢ_empty
deleted theorem Set.bunionᵢ_eq_unionᵢ
deleted theorem Set.bunionᵢ_image
deleted theorem Set.bunionᵢ_insert
deleted theorem Set.bunionᵢ_mono
deleted theorem Set.bunionᵢ_pair
deleted theorem Set.bunionᵢ_range
deleted theorem Set.bunionᵢ_self
deleted theorem Set.bunionᵢ_singleton
deleted theorem Set.bunionᵢ_union
deleted theorem Set.bunionᵢ_unionᵢ
deleted theorem Set.bunionᵢ_univ
added theorem Set.compl_iInter
added theorem Set.compl_iInter₂
added theorem Set.compl_iUnion
added theorem Set.compl_iUnion₂
deleted theorem Set.compl_interᵢ
deleted theorem Set.compl_interᵢ₂
deleted theorem Set.compl_interₛ
added theorem Set.compl_sInter
added theorem Set.compl_sUnion
deleted theorem Set.compl_unionᵢ
deleted theorem Set.compl_unionᵢ₂
deleted theorem Set.compl_unionₛ
added theorem Set.diff_iInter
added theorem Set.diff_iUnion
deleted theorem Set.diff_interᵢ
deleted theorem Set.diff_unionᵢ
added theorem Set.directed_on_iUnion
deleted theorem Set.directed_on_unionᵢ
added theorem Set.iInf_eq_dif
added theorem Set.iInf_eq_iInter
added def Set.iInter
added theorem Set.iInter_and
added theorem Set.iInter_coe_set
added theorem Set.iInter_comm
added theorem Set.iInter_congr
added theorem Set.iInter_congr_Prop
added theorem Set.iInter_const
added theorem Set.iInter_dite
added theorem Set.iInter_eq_const
added theorem Set.iInter_eq_if
added theorem Set.iInter_eq_univ
added theorem Set.iInter_exists
added theorem Set.iInter_false
added theorem Set.iInter_iInter_eq'
added theorem Set.iInter_inter
added theorem Set.iInter_ite
added theorem Set.iInter_mono'
added theorem Set.iInter_mono
added theorem Set.iInter_of_empty
added theorem Set.iInter_option
added theorem Set.iInter_or
added theorem Set.iInter_plift_down
added theorem Set.iInter_plift_up
added theorem Set.iInter_setOf
added theorem Set.iInter_subset
added theorem Set.iInter_subtype
added theorem Set.iInter_true
added theorem Set.iInter_union
added theorem Set.iInter_univ
added theorem Set.iInter₂_comm
added theorem Set.iInter₂_congr
added theorem Set.iInter₂_mono'
added theorem Set.iInter₂_mono
added theorem Set.iInter₂_subset
added theorem Set.iInter₂_union
added theorem Set.iSup_eq_iUnion
added def Set.iUnion
added theorem Set.iUnion_and
added theorem Set.iUnion_coe_set
added theorem Set.iUnion_comm
added theorem Set.iUnion_congr
added theorem Set.iUnion_congr_Prop
added theorem Set.iUnion_const
added theorem Set.iUnion_diff
added theorem Set.iUnion_dite
added theorem Set.iUnion_empty
added theorem Set.iUnion_eq_const
added theorem Set.iUnion_eq_dif
added theorem Set.iUnion_eq_empty
added theorem Set.iUnion_eq_if
added theorem Set.iUnion_eq_univ_iff
added theorem Set.iUnion_exists
added theorem Set.iUnion_false
added theorem Set.iUnion_iUnion_eq'
added theorem Set.iUnion_image_left
added theorem Set.iUnion_image_right
added theorem Set.iUnion_inter
added theorem Set.iUnion_ite
added theorem Set.iUnion_mono'
added theorem Set.iUnion_mono
added theorem Set.iUnion_of_empty
added theorem Set.iUnion_option
added theorem Set.iUnion_or
added theorem Set.iUnion_plift_down
added theorem Set.iUnion_plift_up
added theorem Set.iUnion_prod
added theorem Set.iUnion_prod_const
added theorem Set.iUnion_setOf
added theorem Set.iUnion_subset
added theorem Set.iUnion_subset_iff
added theorem Set.iUnion_subtype
added theorem Set.iUnion_true
added theorem Set.iUnion_union
added theorem Set.iUnion_univ_pi
added theorem Set.iUnion₂_comm
added theorem Set.iUnion₂_congr
added theorem Set.iUnion₂_inter
added theorem Set.iUnion₂_mono'
added theorem Set.iUnion₂_mono
added theorem Set.iUnion₂_subset
added theorem Set.image2_eq_iUnion
deleted theorem Set.image2_eq_unionᵢ
added theorem Set.image2_iUnion_left
deleted theorem Set.image2_unionᵢ_left
deleted theorem Set.image2_unionᵢ_right
added theorem Set.image_eq_iUnion
deleted theorem Set.image_eq_unionᵢ
added theorem Set.image_iInter
added theorem Set.image_iInter₂
added theorem Set.image_iUnion
added theorem Set.image_iUnion₂
deleted theorem Set.image_interᵢ
deleted theorem Set.image_interᵢ_subset
deleted theorem Set.image_interᵢ₂
deleted theorem Set.image_interₛ_subset
deleted theorem Set.image_unionᵢ
deleted theorem Set.image_unionᵢ₂
deleted theorem Set.infᵢ_eq_dif
deleted theorem Set.infᵢ_eq_interᵢ
deleted theorem Set.infₛ_eq_interₛ
added theorem Set.inter_biInter
deleted theorem Set.inter_binterᵢ
added theorem Set.inter_eq_iInter
deleted theorem Set.inter_eq_interᵢ
added theorem Set.inter_iInter
added theorem Set.inter_iUnion
added theorem Set.inter_iUnion₂
deleted theorem Set.inter_interᵢ
deleted theorem Set.inter_unionᵢ
deleted theorem Set.inter_unionᵢ₂
deleted def Set.interᵢ
deleted theorem Set.interᵢ_and
deleted theorem Set.interᵢ_coe_set
deleted theorem Set.interᵢ_comm
deleted theorem Set.interᵢ_congr
deleted theorem Set.interᵢ_congr_Prop
deleted theorem Set.interᵢ_const
deleted theorem Set.interᵢ_dite
deleted theorem Set.interᵢ_eq_const
deleted theorem Set.interᵢ_eq_empty_iff
deleted theorem Set.interᵢ_eq_if
deleted theorem Set.interᵢ_eq_univ
deleted theorem Set.interᵢ_exists
deleted theorem Set.interᵢ_false
deleted theorem Set.interᵢ_inter
deleted theorem Set.interᵢ_interᵢ_eq'
deleted theorem Set.interᵢ_ite
deleted theorem Set.interᵢ_mono'
deleted theorem Set.interᵢ_mono
deleted theorem Set.interᵢ_of_empty
deleted theorem Set.interᵢ_option
deleted theorem Set.interᵢ_or
deleted theorem Set.interᵢ_plift_down
deleted theorem Set.interᵢ_plift_up
deleted theorem Set.interᵢ_setOf
deleted theorem Set.interᵢ_subset
deleted theorem Set.interᵢ_subtype
deleted theorem Set.interᵢ_true
deleted theorem Set.interᵢ_union
deleted theorem Set.interᵢ_univ
deleted theorem Set.interᵢ₂_comm
deleted theorem Set.interᵢ₂_congr
deleted theorem Set.interᵢ₂_mono'
deleted theorem Set.interᵢ₂_mono
deleted theorem Set.interᵢ₂_subset
deleted theorem Set.interᵢ₂_union
deleted def Set.interₛ
deleted theorem Set.interₛ_empty
deleted theorem Set.interₛ_eq_binterᵢ
deleted theorem Set.interₛ_eq_empty_iff
deleted theorem Set.interₛ_eq_interᵢ
deleted theorem Set.interₛ_eq_univ
deleted theorem Set.interₛ_image
deleted theorem Set.interₛ_insert
deleted theorem Set.interₛ_pair
deleted theorem Set.interₛ_prod
deleted theorem Set.interₛ_range
deleted theorem Set.interₛ_singleton
deleted theorem Set.interₛ_union
deleted theorem Set.interₛ_unionᵢ
added theorem Set.mapsTo_iInter
added theorem Set.mapsTo_iInter₂
added theorem Set.mapsTo_iUnion
added theorem Set.mapsTo_iUnion₂
deleted theorem Set.mapsTo_interᵢ
deleted theorem Set.mapsTo_interᵢ₂
deleted theorem Set.mapsTo_interₛ
added theorem Set.mapsTo_sInter
added theorem Set.mapsTo_sUnion
deleted theorem Set.mapsTo_unionᵢ
deleted theorem Set.mapsTo_unionᵢ₂
deleted theorem Set.mapsTo_unionₛ
added theorem Set.mem_biInter
added theorem Set.mem_biUnion
deleted theorem Set.mem_binterᵢ
deleted theorem Set.mem_bunionᵢ
added theorem Set.mem_iInter
added theorem Set.mem_iInter_of_mem
added theorem Set.mem_iInter₂
added theorem Set.mem_iUnion
added theorem Set.mem_iUnion_of_mem
added theorem Set.mem_iUnion₂
deleted theorem Set.mem_interᵢ
deleted theorem Set.mem_interᵢ_of_mem
deleted theorem Set.mem_interᵢ₂
deleted theorem Set.mem_interₛ
added theorem Set.mem_sInter
added theorem Set.mem_sUnion
added theorem Set.mem_sUnion_of_mem
deleted theorem Set.mem_unionᵢ
deleted theorem Set.mem_unionᵢ_of_mem
deleted theorem Set.mem_unionᵢ₂
deleted theorem Set.mem_unionₛ
deleted theorem Set.mem_unionₛ_of_mem
added theorem Set.nonempty_biUnion
deleted theorem Set.nonempty_bunionᵢ
added theorem Set.nonempty_iInter
added theorem Set.nonempty_iInter₂
added theorem Set.nonempty_iUnion
deleted theorem Set.nonempty_interᵢ
deleted theorem Set.nonempty_interᵢ₂
deleted theorem Set.nonempty_interₛ
added theorem Set.nonempty_sInter
added theorem Set.nonempty_sUnion
deleted theorem Set.nonempty_unionᵢ
deleted theorem Set.nonempty_unionₛ
added theorem Set.preimage_iInter
added theorem Set.preimage_iInter₂
added theorem Set.preimage_iUnion
added theorem Set.preimage_iUnion₂
deleted theorem Set.preimage_interᵢ
deleted theorem Set.preimage_interᵢ₂
deleted theorem Set.preimage_interₛ
added theorem Set.preimage_sInter
added theorem Set.preimage_sUnion
deleted theorem Set.preimage_unionᵢ
deleted theorem Set.preimage_unionᵢ₂
deleted theorem Set.preimage_unionₛ
added theorem Set.prod_iUnion
added theorem Set.prod_iUnion₂
deleted theorem Set.prod_interₛ
added theorem Set.prod_sInter
added theorem Set.prod_sUnion
deleted theorem Set.prod_unionᵢ
deleted theorem Set.prod_unionᵢ₂
deleted theorem Set.prod_unionₛ
added theorem Set.range_eq_iUnion
deleted theorem Set.range_eq_unionᵢ
added theorem Set.sInf_eq_sInter
added def Set.sInter
added theorem Set.sInter_empty
added theorem Set.sInter_eq_biInter
added theorem Set.sInter_eq_iInter
added theorem Set.sInter_eq_univ
added theorem Set.sInter_iUnion
added theorem Set.sInter_image
added theorem Set.sInter_insert
added theorem Set.sInter_pair
added theorem Set.sInter_prod
added theorem Set.sInter_prod_sInter
added theorem Set.sInter_range
added theorem Set.sInter_singleton
added theorem Set.sInter_union
added theorem Set.sSup_eq_sUnion
added def Set.sUnion
added theorem Set.sUnion_empty
added theorem Set.sUnion_eq_biUnion
added theorem Set.sUnion_eq_empty
added theorem Set.sUnion_eq_iUnion
added theorem Set.sUnion_eq_univ_iff
added theorem Set.sUnion_iUnion
added theorem Set.sUnion_image
added theorem Set.sUnion_insert
added theorem Set.sUnion_mono
added theorem Set.sUnion_pair
added theorem Set.sUnion_prod_const
added theorem Set.sUnion_range
added theorem Set.sUnion_singleton
added theorem Set.sUnion_subset
added theorem Set.sUnion_subset_iff
added theorem Set.sUnion_union
deleted def Set.sigmaToUnionᵢ
added theorem Set.subset_iInter
added theorem Set.subset_iInter_iff
added theorem Set.subset_iInter₂
added theorem Set.subset_iUnion
added theorem Set.subset_iUnion₂
deleted theorem Set.subset_interᵢ
deleted theorem Set.subset_interᵢ_iff
deleted theorem Set.subset_interᵢ₂
deleted theorem Set.subset_interₛ
deleted theorem Set.subset_interₛ_iff
added theorem Set.subset_sInter
added theorem Set.subset_sInter_iff
deleted theorem Set.subset_unionᵢ
deleted theorem Set.subset_unionᵢ₂
deleted theorem Set.supᵢ_eq_unionᵢ
deleted theorem Set.supₛ_eq_unionₛ
added theorem Set.surjOn_iInter
added theorem Set.surjOn_iUnion
added theorem Set.surjOn_iUnion₂
deleted theorem Set.surjOn_interᵢ
added theorem Set.surjOn_sUnion
deleted theorem Set.surjOn_unionᵢ
deleted theorem Set.surjOn_unionᵢ₂
deleted theorem Set.surjOn_unionₛ
added theorem Set.union_eq_iUnion
deleted theorem Set.union_eq_unionᵢ
added theorem Set.union_iInter
added theorem Set.union_iInter₂
added theorem Set.union_iUnion
deleted theorem Set.union_interᵢ
deleted theorem Set.union_interᵢ₂
deleted theorem Set.union_unionᵢ
deleted def Set.unionᵢ
deleted theorem Set.unionᵢ_and
deleted theorem Set.unionᵢ_coe_set
deleted theorem Set.unionᵢ_comm
deleted theorem Set.unionᵢ_congr
deleted theorem Set.unionᵢ_congr_Prop
deleted theorem Set.unionᵢ_const
deleted theorem Set.unionᵢ_diff
deleted theorem Set.unionᵢ_dite
deleted theorem Set.unionᵢ_empty
deleted theorem Set.unionᵢ_eq_const
deleted theorem Set.unionᵢ_eq_dif
deleted theorem Set.unionᵢ_eq_empty
deleted theorem Set.unionᵢ_eq_if
deleted theorem Set.unionᵢ_eq_univ_iff
deleted theorem Set.unionᵢ_exists
deleted theorem Set.unionᵢ_false
deleted theorem Set.unionᵢ_image_left
deleted theorem Set.unionᵢ_image_right
deleted theorem Set.unionᵢ_inter
deleted theorem Set.unionᵢ_inter_subset
deleted theorem Set.unionᵢ_ite
deleted theorem Set.unionᵢ_mono'
deleted theorem Set.unionᵢ_mono
deleted theorem Set.unionᵢ_of_empty
deleted theorem Set.unionᵢ_of_singleton
deleted theorem Set.unionᵢ_option
deleted theorem Set.unionᵢ_or
deleted theorem Set.unionᵢ_plift_down
deleted theorem Set.unionᵢ_plift_up
deleted theorem Set.unionᵢ_prod
deleted theorem Set.unionᵢ_prod_const
deleted theorem Set.unionᵢ_setOf
deleted theorem Set.unionᵢ_subset
deleted theorem Set.unionᵢ_subset_iff
deleted theorem Set.unionᵢ_subtype
deleted theorem Set.unionᵢ_true
deleted theorem Set.unionᵢ_union
deleted theorem Set.unionᵢ_unionᵢ_eq'
deleted theorem Set.unionᵢ_univ_pi
deleted theorem Set.unionᵢ₂_comm
deleted theorem Set.unionᵢ₂_congr
deleted theorem Set.unionᵢ₂_inter
deleted theorem Set.unionᵢ₂_mono'
deleted theorem Set.unionᵢ₂_mono
deleted theorem Set.unionᵢ₂_subset
deleted def Set.unionₛ
deleted theorem Set.unionₛ_empty
deleted theorem Set.unionₛ_eq_bunionᵢ
deleted theorem Set.unionₛ_eq_empty
deleted theorem Set.unionₛ_eq_unionᵢ
deleted theorem Set.unionₛ_eq_univ_iff
deleted theorem Set.unionₛ_image
deleted theorem Set.unionₛ_insert
deleted theorem Set.unionₛ_mono
deleted theorem Set.unionₛ_pair
deleted theorem Set.unionₛ_prod_const
deleted theorem Set.unionₛ_range
deleted theorem Set.unionₛ_singleton
deleted theorem Set.unionₛ_subset
deleted theorem Set.unionₛ_subset_iff
deleted theorem Set.unionₛ_union
deleted theorem Set.unionₛ_unionᵢ
added theorem Set.univ_pi_eq_iInter
deleted theorem Set.univ_pi_eq_interᵢ
added theorem iInf_iUnion
added theorem iSup_iUnion
deleted theorem infᵢ_unionᵢ
deleted theorem infₛ_unionₛ
added theorem sInf_sUnion
added theorem sSup_sUnion
deleted theorem supᵢ_unionᵢ
deleted theorem supₛ_unionₛ
added theorem Set.pairwise_iUnion
added theorem Set.pairwise_sUnion
deleted theorem Set.pairwise_unionᵢ
deleted theorem Set.pairwise_unionₛ
added theorem Set.div_iInter_subset
added theorem Set.div_iUnion
added theorem Set.div_iUnion₂
deleted theorem Set.div_interᵢ_subset
deleted theorem Set.div_unionᵢ
deleted theorem Set.div_unionᵢ₂
added theorem Set.iInter_div_subset
added theorem Set.iInter_inv
added theorem Set.iInter_mul_subset
added theorem Set.iUnion_div
added theorem Set.iUnion_inv
added theorem Set.iUnion_mul
added theorem Set.iUnion₂_div
added theorem Set.iUnion₂_mul
deleted theorem Set.interᵢ_div_subset
deleted theorem Set.interᵢ_inv
deleted theorem Set.interᵢ_mul_subset
added theorem Set.mul_iInter_subset
added theorem Set.mul_iUnion
added theorem Set.mul_iUnion₂
deleted theorem Set.mul_interᵢ_subset
deleted theorem Set.mul_unionᵢ
deleted theorem Set.mul_unionᵢ₂
deleted theorem Set.unionᵢ_div
deleted theorem Set.unionᵢ_inv
deleted theorem Set.unionᵢ_mul
deleted theorem Set.unionᵢ₂_div
deleted theorem Set.unionᵢ₂_mul
added theorem Set.iInter_smul_subset
added theorem Set.iInter_vsub_subset
added theorem Set.iUnion_inv_smul
added theorem Set.iUnion_op_smul_set
added theorem Set.iUnion_smul
added theorem Set.iUnion_smul_set
added theorem Set.iUnion_vsub
added theorem Set.iUnion₂_smul
added theorem Set.iUnion₂_vsub
deleted theorem Set.interᵢ_smul_subset
deleted theorem Set.interᵢ_vsub_subset
added theorem Set.smul_iInter_subset
added theorem Set.smul_iUnion
added theorem Set.smul_iUnion₂
deleted theorem Set.smul_interᵢ_subset
added theorem Set.smul_set_iUnion₂
deleted theorem Set.smul_set_unionᵢ₂
deleted theorem Set.smul_unionᵢ
deleted theorem Set.smul_unionᵢ₂
deleted theorem Set.unionᵢ_inv_smul
deleted theorem Set.unionᵢ_op_smul_set
deleted theorem Set.unionᵢ_smul
deleted theorem Set.unionᵢ_smul_set
deleted theorem Set.unionᵢ_vsub
deleted theorem Set.unionᵢ₂_smul
deleted theorem Set.unionᵢ₂_vsub
added theorem Set.vsub_iInter_subset
added theorem Set.vsub_iUnion
added theorem Set.vsub_iUnion₂
deleted theorem Set.vsub_interᵢ_subset
deleted theorem Set.vsub_unionᵢ
deleted theorem Set.vsub_unionᵢ₂
added theorem Set.iUnionLift_binary
added theorem Set.iUnionLift_const
added theorem Set.iUnionLift_mk
added theorem Set.iUnionLift_of_mem
added theorem Set.iUnionLift_unary
deleted theorem Set.preimage_unionᵢLift
deleted theorem Set.unionᵢLift_binary
deleted theorem Set.unionᵢLift_const
deleted theorem Set.unionᵢLift_mk
deleted theorem Set.unionᵢLift_of_mem
deleted theorem Set.unionᵢLift_unary
deleted theorem Setoid.infₛ_def
added theorem Setoid.sInf_def
added theorem Setoid.sSup_def
added theorem Setoid.sSup_eq_eqvGen
deleted theorem Setoid.supₛ_def
deleted theorem Setoid.supₛ_eq_eqvGen
deleted theorem IndexedPartition.unionᵢ
added theorem Setoid.sUnion_classes
deleted theorem Setoid.unionₛ_classes
added theorem IsSubfield.iInter
deleted theorem IsSubfield.interᵢ
added theorem IsSubgroup.iInter
deleted theorem IsSubgroup.interᵢ
added theorem IsSubmonoid.iInter
deleted theorem IsSubmonoid.interᵢ
added theorem IsSubring.iInter
deleted theorem IsSubring.interᵢ
added theorem IsOpen.iUnion_smul
deleted theorem IsOpen.unionᵢ_smul
added theorem omegaLimit_eq_iInter
deleted theorem omegaLimit_eq_interᵢ
added theorem omegaLimit_iInter
added theorem omegaLimit_iUnion
deleted theorem omegaLimit_interᵢ
deleted theorem omegaLimit_unionᵢ
deleted theorem Subfield.closure_unionᵢ
deleted theorem Subfield.closure_unionₛ
deleted theorem Subfield.coe_infₛ
added theorem Subfield.coe_sInf
added theorem Subfield.comap_iInf
deleted theorem Subfield.comap_infᵢ
deleted theorem Subfield.infₛ_toSubring
deleted theorem Subfield.isGLB_infₛ
added theorem Subfield.isGLB_sInf
added theorem Subfield.map_iSup
deleted theorem Subfield.map_supᵢ
deleted theorem Subfield.mem_infₛ
added theorem Subfield.mem_sInf
modified theorem Con.conGen_eq
deleted theorem Con.infₛ_def
deleted theorem Con.infₛ_toSetoid
added theorem Con.sInf_def
added theorem Con.sInf_toSetoid
added theorem Con.sSup_def
added theorem Con.sSup_eq_conGen
deleted theorem Con.supₛ_def
deleted theorem Con.supₛ_eq_conGen
added theorem fixingSubgroup_iUnion
deleted theorem fixingSubgroup_unionᵢ
added theorem fixingSubmonoid_iUnion
deleted theorem fixingSubmonoid_unionᵢ
added theorem Subgroup.index_iInf_le
deleted theorem Subgroup.index_infᵢ_le
deleted theorem Subgroup.closure_unionᵢ
added theorem Subgroup.coe_iInf
deleted theorem Subgroup.coe_infᵢ
deleted theorem Subgroup.coe_infₛ
added theorem Subgroup.coe_sInf
added theorem Subgroup.comap_iInf
deleted theorem Subgroup.comap_infᵢ
added theorem Subgroup.iSup_comap_le
added theorem Subgroup.map_iSup
deleted theorem Subgroup.map_supᵢ
added theorem Subgroup.mem_iInf
deleted theorem Subgroup.mem_infᵢ
deleted theorem Subgroup.mem_infₛ
added theorem Subgroup.mem_sInf
deleted theorem Subgroup.supᵢ_comap_le
deleted theorem Subgroup.supᵢ_induction
deleted theorem Subgroup.center_eq_infᵢ
added theorem Submonoid.coe_iInf
deleted theorem Submonoid.coe_infᵢ
deleted theorem Submonoid.coe_infₛ
added theorem Submonoid.coe_sInf
added theorem Submonoid.mem_iInf
added theorem Submonoid.mem_iSup
deleted theorem Submonoid.mem_infᵢ
deleted theorem Submonoid.mem_infₛ
added theorem Submonoid.mem_sInf
deleted theorem Submonoid.mem_supᵢ
added theorem Submonoid.comap_iInf
deleted theorem Submonoid.comap_infᵢ
added theorem Submonoid.map_iSup
deleted theorem Submonoid.map_supᵢ
added theorem Submonoid.inv_iInf
added theorem Submonoid.inv_iSup
deleted theorem Submonoid.inv_infᵢ
deleted theorem Submonoid.inv_supᵢ
added theorem Subsemigroup.coe_iInf
deleted theorem Subsemigroup.coe_infᵢ
deleted theorem Subsemigroup.coe_infₛ
added theorem Subsemigroup.coe_sInf
added theorem Subsemigroup.mem_iInf
added theorem Subsemigroup.mem_iSup
deleted theorem Subsemigroup.mem_infᵢ
deleted theorem Subsemigroup.mem_infₛ
added theorem Subsemigroup.mem_sInf
deleted theorem Subsemigroup.mem_supᵢ
deleted theorem Subsemigroup.comap_infᵢ
added theorem Subsemigroup.map_iSup
deleted theorem Subsemigroup.map_supᵢ
deleted theorem AffineSubspace.map_supᵢ
added theorem Submodule.comap_iInf
deleted theorem Submodule.comap_infᵢ
added theorem Submodule.map_iSup
deleted theorem Submodule.map_supᵢ
deleted theorem LinearMap.infᵢ_ker_proj
added theorem Submodule.iSup_eq_span
added theorem Submodule.iSup_span
added theorem Submodule.mem_iSup
deleted theorem Submodule.mem_supᵢ
added theorem Submodule.span_iUnion
deleted theorem Submodule.span_unionᵢ
deleted theorem Submodule.supᵢ_eq_span
deleted theorem Submodule.supᵢ_span
added theorem aeSeq.iSup
deleted theorem aeSeq.supᵢ
added theorem measurable_iUnionLift
deleted theorem measurable_unionᵢLift
added theorem MeasurableSet.biInter
deleted theorem MeasurableSet.binterᵢ
added theorem MeasurableSet.iInter
deleted theorem MeasurableSet.interᵢ
deleted theorem MeasurableSet.interₛ
added theorem MeasurableSet.sInter
deleted theorem aemeasurable_unionᵢ_iff
deleted def piUnionᵢInter
deleted theorem piUnionᵢInter_mono_left
deleted theorem piUnionᵢInter_singleton
added def piiUnionInter
deleted theorem subset_piUnionᵢInter
added theorem subset_piiUnionInter
added theorem sSup_atoms_eq_top
added theorem sSup_atoms_le_eq
deleted theorem supₛ_atoms_eq_top
deleted theorem supₛ_atoms_le_eq
added theorem DirectedOn.inf_sSup_eq
deleted theorem DirectedOn.inf_supₛ_eq
added theorem sSup_compact_eq_top
added theorem sSup_compact_le_eq
deleted theorem supₛ_compact_eq_top
deleted theorem supₛ_compact_le_eq
deleted theorem PUnit.infₛ_eq
added theorem PUnit.sInf_eq
added theorem PUnit.sSup_eq
deleted theorem PUnit.supₛ_eq
added theorem biInf_sup_biInf
added theorem biSup_inf_biSup
deleted theorem binfᵢ_sup_binfᵢ
deleted theorem bsupᵢ_inf_bsupᵢ
added theorem compl_iInf
added theorem compl_iSup
deleted theorem compl_infᵢ
deleted theorem compl_infₛ'
deleted theorem compl_infₛ
added theorem compl_sInf'
added theorem compl_sInf
added theorem compl_sSup'
added theorem compl_sSup
deleted theorem compl_supᵢ
deleted theorem compl_supₛ'
deleted theorem compl_supₛ
added theorem disjoint_iSup_iff
added theorem disjoint_iSup₂_iff
added theorem disjoint_sSup_iff
deleted theorem disjoint_supᵢ_iff
deleted theorem disjoint_supᵢ₂_iff
deleted theorem disjoint_supₛ_iff
added theorem iInf_sup_eq
added theorem iInf_sup_iInf
added theorem iInf_sup_of_antitone
added theorem iInf_sup_of_monotone
added theorem iInf₂_sup_eq
added theorem iSup_disjoint_iff
added theorem iSup_inf_eq
added theorem iSup_inf_iSup
added theorem iSup_inf_of_antitone
added theorem iSup_inf_of_monotone
added theorem iSup₂_disjoint_iff
added theorem iSup₂_inf_eq
added theorem inf_iSup_eq
added theorem inf_iSup₂_eq
added theorem inf_sSup_eq
deleted theorem inf_supᵢ_eq
deleted theorem inf_supᵢ₂_eq
deleted theorem inf_supₛ_eq
deleted theorem infᵢ_sup_eq
deleted theorem infᵢ_sup_infᵢ
deleted theorem infᵢ_sup_of_antitone
deleted theorem infᵢ_sup_of_monotone
deleted theorem infᵢ₂_sup_eq
deleted theorem infₛ_sup_eq
deleted theorem infₛ_sup_infₛ
added theorem sInf_sup_eq
added theorem sInf_sup_sInf
added theorem sSup_disjoint_iff
added theorem sSup_inf_eq
added theorem sSup_inf_sSup
added theorem sup_iInf_eq
added theorem sup_iInf₂_eq
deleted theorem sup_infᵢ_eq
deleted theorem sup_infᵢ₂_eq
deleted theorem sup_infₛ_eq
added theorem sup_sInf_eq
deleted theorem supᵢ_disjoint_iff
deleted theorem supᵢ_inf_eq
deleted theorem supᵢ_inf_of_antitone
deleted theorem supᵢ_inf_of_monotone
deleted theorem supᵢ_inf_supᵢ
deleted theorem supᵢ₂_disjoint_iff
deleted theorem supᵢ₂_inf_eq
deleted theorem supₛ_disjoint_iff
deleted theorem supₛ_inf_eq
deleted theorem supₛ_inf_supₛ
added theorem Antitone.iInf_nat_add
deleted theorem Antitone.infᵢ_nat_add
added theorem Antitone.le_map_iInf
deleted theorem Antitone.le_map_infᵢ
deleted theorem Antitone.le_map_infᵢ₂
deleted theorem Antitone.le_map_infₛ
added theorem Antitone.le_map_sInf
added theorem Antitone.map_iSup_le
added theorem Antitone.map_sSup_le
deleted theorem Antitone.map_supᵢ_le
deleted theorem Antitone.map_supᵢ₂_le
deleted theorem Antitone.map_supₛ_le
added theorem Equiv.iInf_comp
added theorem Equiv.iSup_comp
deleted theorem Equiv.infᵢ_comp
deleted theorem Equiv.supᵢ_comp
added theorem IsGLB.iInf_eq
deleted theorem IsGLB.infᵢ_eq
deleted theorem IsGLB.infₛ_eq
added theorem IsGLB.sInf_eq
added theorem IsLUB.iSup_eq
added theorem IsLUB.sSup_eq
deleted theorem IsLUB.supᵢ_eq
deleted theorem IsLUB.supₛ_eq
added theorem Monotone.iInf_comp_eq
added theorem Monotone.iSup_comp_eq
added theorem Monotone.iSup_nat_add
deleted theorem Monotone.infᵢ_comp_eq
added theorem Monotone.le_map_iSup
added theorem Monotone.le_map_sSup
deleted theorem Monotone.le_map_supᵢ
deleted theorem Monotone.le_map_supᵢ₂
deleted theorem Monotone.le_map_supₛ
added theorem Monotone.map_iInf_le
deleted theorem Monotone.map_infᵢ_le
deleted theorem Monotone.map_infᵢ₂_le
deleted theorem Monotone.map_infₛ_le
added theorem Monotone.map_sInf_le
deleted theorem Monotone.supᵢ_comp_eq
deleted theorem Monotone.supᵢ_nat_add
added theorem OrderIso.map_iInf
added theorem OrderIso.map_iSup
deleted theorem OrderIso.map_infᵢ
deleted theorem OrderIso.map_infₛ
added theorem OrderIso.map_sInf
added theorem OrderIso.map_sSup
deleted theorem OrderIso.map_supᵢ
deleted theorem OrderIso.map_supₛ
added theorem Prod.fst_iInf
added theorem Prod.fst_iSup
deleted theorem Prod.fst_infᵢ
deleted theorem Prod.fst_infₛ
added theorem Prod.fst_sInf
added theorem Prod.fst_sSup
deleted theorem Prod.fst_supᵢ
deleted theorem Prod.fst_supₛ
added theorem Prod.iInf_mk
added theorem Prod.iSup_mk
deleted theorem Prod.infᵢ_mk
added theorem Prod.snd_iInf
added theorem Prod.snd_iSup
deleted theorem Prod.snd_infᵢ
deleted theorem Prod.snd_infₛ
added theorem Prod.snd_sInf
added theorem Prod.snd_sSup
deleted theorem Prod.snd_supᵢ
deleted theorem Prod.snd_supₛ
deleted theorem Prod.supᵢ_mk
added theorem Prod.swap_iInf
added theorem Prod.swap_iSup
deleted theorem Prod.swap_infᵢ
deleted theorem Prod.swap_infₛ
added theorem Prod.swap_sInf
added theorem Prod.swap_sSup
deleted theorem Prod.swap_supᵢ
deleted theorem Prod.swap_supₛ
added theorem biInf_const
added theorem biInf_inf
added theorem biInf_mono
added theorem biInf_prod
added theorem biSup_const
added theorem biSup_mono
added theorem biSup_prod
added theorem biSup_sup
deleted theorem binfᵢ_const
deleted theorem binfᵢ_inf
deleted theorem binfᵢ_mono
deleted theorem binfᵢ_prod
deleted theorem bsupᵢ_const
deleted theorem bsupᵢ_mono
deleted theorem bsupᵢ_prod
deleted theorem bsupᵢ_sup
added theorem disjoint_sSup_left
added theorem disjoint_sSup_right
deleted theorem disjoint_supₛ_left
deleted theorem disjoint_supₛ_right
added def iInf.unexpander
added def iInf
added theorem iInf_Prop_eq
added theorem iInf_and'
added theorem iInf_and
added theorem iInf_apply
added theorem iInf_bool_eq
added theorem iInf_comm
added theorem iInf_congr
added theorem iInf_congr_Prop
added theorem iInf_const
added theorem iInf_const_mono
added theorem iInf_dite
added theorem iInf_emptyset
added theorem iInf_eq_bot
added theorem iInf_eq_dif
added theorem iInf_eq_if
added theorem iInf_eq_top
added theorem iInf_exists
added theorem iInf_extend_top
added theorem iInf_false
added theorem iInf_iInf_eq_left
added theorem iInf_iInf_eq_right
added theorem iInf_iSup_ge_nat_add
added theorem iInf_image
added theorem iInf_inf
added theorem iInf_inf_eq
added theorem iInf_insert
added theorem iInf_ite
added theorem iInf_le'
added theorem iInf_le
added theorem iInf_le_iInf_of_subset
added theorem iInf_le_iInf₂
added theorem iInf_le_iff
added theorem iInf_le_of_le
added theorem iInf_lt_iff
added theorem iInf_mono'
added theorem iInf_mono
added theorem iInf_nat_gt_zero_eq
added theorem iInf_ne_top_subtype
added theorem iInf_neg
added theorem iInf_of_empty'
added theorem iInf_of_empty
added theorem iInf_option
added theorem iInf_option_elim
added theorem iInf_or
added theorem iInf_pair
added theorem iInf_plift_down
added theorem iInf_plift_up
added theorem iInf_pos
added theorem iInf_prod
added theorem iInf_range'
added theorem iInf_range
added theorem iInf_sigma
added theorem iInf_singleton
added theorem iInf_split
added theorem iInf_split_single
added theorem iInf_subtype''
added theorem iInf_subtype'
added theorem iInf_subtype
added theorem iInf_sum
added theorem iInf_sup_iInf_le
added theorem iInf_top
added theorem iInf_true
added theorem iInf_union
added theorem iInf_univ
added theorem iInf₂_comm
added theorem iInf₂_eq_top
added theorem iInf₂_le
added theorem iInf₂_le_of_le
added theorem iInf₂_mono'
added theorem iInf₂_mono
added def iSup.unexpander
added def iSup
added theorem iSup_Prop_eq
added theorem iSup_and'
added theorem iSup_and
added theorem iSup_apply
added theorem iSup_bool_eq
added theorem iSup_bot
added theorem iSup_comm
added theorem iSup_comp_le
added theorem iSup_congr
added theorem iSup_congr_Prop
added theorem iSup_const
added theorem iSup_const_le
added theorem iSup_const_mono
added theorem iSup_dite
added theorem iSup_emptyset
added theorem iSup_eq_bot
added theorem iSup_eq_dif
added theorem iSup_eq_if
added theorem iSup_eq_top
added theorem iSup_exists
added theorem iSup_extend_bot
added theorem iSup_false
added theorem iSup_iInf_ge_nat_add
added theorem iSup_iInf_le_iInf_iSup
added theorem iSup_iSup_eq_left
added theorem iSup_iSup_eq_right
added theorem iSup_image
added theorem iSup_inf_le_inf_sSup
added theorem iSup_inf_le_sSup_inf
added theorem iSup_insert
added theorem iSup_ite
added theorem iSup_le
added theorem iSup_le_iSup_of_subset
added theorem iSup_le_iff
added theorem iSup_lt_iff
added theorem iSup_mono'
added theorem iSup_mono
added theorem iSup_nat_gt_zero_eq
added theorem iSup_ne_bot_subtype
added theorem iSup_neg
added theorem iSup_of_empty'
added theorem iSup_of_empty
added theorem iSup_option
added theorem iSup_option_elim
added theorem iSup_or
added theorem iSup_pair
added theorem iSup_plift_down
added theorem iSup_plift_up
added theorem iSup_pos
added theorem iSup_prod
added theorem iSup_range'
added theorem iSup_range
added theorem iSup_sigma
added theorem iSup_singleton
added theorem iSup_split
added theorem iSup_split_single
added theorem iSup_subtype''
added theorem iSup_subtype'
added theorem iSup_subtype
added theorem iSup_sum
added theorem iSup_sup
added theorem iSup_sup_eq
added theorem iSup_true
added theorem iSup_union
added theorem iSup_univ
added theorem iSup₂_comm
added theorem iSup₂_eq_bot
added theorem iSup₂_le
added theorem iSup₂_le_iSup
added theorem iSup₂_le_iff
added theorem iSup₂_mono'
added theorem iSup₂_mono
added theorem inf_biInf
deleted theorem inf_binfᵢ
added theorem inf_eq_iInf
deleted theorem inf_eq_infᵢ
added theorem inf_iInf
added theorem inf_iInf_nat_succ
deleted theorem inf_infᵢ
deleted theorem inf_infᵢ_nat_succ
deleted def infᵢ.unexpander
deleted def infᵢ
deleted theorem infᵢ_Prop_eq
deleted theorem infᵢ_and'
deleted theorem infᵢ_and
deleted theorem infᵢ_apply
deleted theorem infᵢ_bool_eq
deleted theorem infᵢ_comm
deleted theorem infᵢ_congr
deleted theorem infᵢ_congr_Prop
deleted theorem infᵢ_const
deleted theorem infᵢ_const_mono
deleted theorem infᵢ_dite
deleted theorem infᵢ_emptyset
deleted theorem infᵢ_eq_bot
deleted theorem infᵢ_eq_dif
deleted theorem infᵢ_eq_if
deleted theorem infᵢ_eq_top
deleted theorem infᵢ_exists
deleted theorem infᵢ_extend_top
deleted theorem infᵢ_false
deleted theorem infᵢ_image
deleted theorem infᵢ_inf
deleted theorem infᵢ_inf_eq
deleted theorem infᵢ_infᵢ_eq_left
deleted theorem infᵢ_infᵢ_eq_right
deleted theorem infᵢ_insert
deleted theorem infᵢ_ite
deleted theorem infᵢ_le'
deleted theorem infᵢ_le
deleted theorem infᵢ_le_iff
deleted theorem infᵢ_le_infᵢ₂
deleted theorem infᵢ_le_of_le
deleted theorem infᵢ_lt_iff
deleted theorem infᵢ_mono'
deleted theorem infᵢ_mono
deleted theorem infᵢ_nat_gt_zero_eq
deleted theorem infᵢ_ne_top_subtype
deleted theorem infᵢ_neg
deleted theorem infᵢ_of_empty'
deleted theorem infᵢ_of_empty
deleted theorem infᵢ_option
deleted theorem infᵢ_option_elim
deleted theorem infᵢ_or
deleted theorem infᵢ_pair
deleted theorem infᵢ_plift_down
deleted theorem infᵢ_plift_up
deleted theorem infᵢ_pos
deleted theorem infᵢ_prod
deleted theorem infᵢ_range'
deleted theorem infᵢ_range
deleted theorem infᵢ_sigma
deleted theorem infᵢ_singleton
deleted theorem infᵢ_split
deleted theorem infᵢ_split_single
deleted theorem infᵢ_subtype''
deleted theorem infᵢ_subtype'
deleted theorem infᵢ_subtype
deleted theorem infᵢ_sum
deleted theorem infᵢ_sup_infᵢ_le
deleted theorem infᵢ_supᵢ_ge_nat_add
deleted theorem infᵢ_top
deleted theorem infᵢ_true
deleted theorem infᵢ_union
deleted theorem infᵢ_univ
deleted theorem infᵢ₂_comm
deleted theorem infᵢ₂_eq_top
deleted theorem infᵢ₂_le
deleted theorem infᵢ₂_le_of_le
deleted theorem infᵢ₂_mono'
deleted theorem infᵢ₂_mono
deleted theorem infₛ_Prop_eq
deleted theorem infₛ_apply
deleted theorem infₛ_diff_singleton_top
deleted theorem infₛ_empty
deleted theorem infₛ_eq_bot
deleted theorem infₛ_eq_infᵢ'
deleted theorem infₛ_eq_infᵢ
deleted theorem infₛ_eq_top
deleted theorem infₛ_image'
deleted theorem infₛ_image2
deleted theorem infₛ_image
deleted theorem infₛ_insert
deleted theorem infₛ_le
deleted theorem infₛ_le_iff
deleted theorem infₛ_le_infₛ
deleted theorem infₛ_le_of_le
deleted theorem infₛ_le_supₛ
deleted theorem infₛ_lt_iff
deleted theorem infₛ_pair
deleted theorem infₛ_prod
deleted theorem infₛ_range
deleted theorem infₛ_singleton
deleted theorem infₛ_sup_le_infᵢ_sup
deleted theorem infₛ_union
deleted theorem infₛ_univ
added theorem isGLB_biInf
deleted theorem isGLB_binfᵢ
added theorem isGLB_iInf
deleted theorem isGLB_infᵢ
deleted theorem isGLB_infₛ
added theorem isGLB_sInf
added theorem isLUB_biSup
deleted theorem isLUB_bsupᵢ
added theorem isLUB_iSup
added theorem isLUB_sSup
deleted theorem isLUB_supᵢ
deleted theorem isLUB_supₛ
added theorem le_iInf
added theorem le_iInf_comp
added theorem le_iInf_const
added theorem le_iInf_iff
added theorem le_iInf₂
added theorem le_iInf₂_iff
added theorem le_iSup'
added theorem le_iSup
added theorem le_iSup_iff
added theorem le_iSup_inf_iSup
added theorem le_iSup_of_le
added theorem le_iSup₂
added theorem le_iSup₂_of_le
deleted theorem le_infᵢ
deleted theorem le_infᵢ_comp
deleted theorem le_infᵢ_const
deleted theorem le_infᵢ_iff
deleted theorem le_infᵢ₂
deleted theorem le_infᵢ₂_iff
deleted theorem le_infₛ
deleted theorem le_infₛ_iff
deleted theorem le_infₛ_inter
added theorem le_sInf
added theorem le_sInf_iff
added theorem le_sInf_inter
added theorem le_sSup
added theorem le_sSup_iff
added theorem le_sSup_of_le
deleted theorem le_supᵢ'
deleted theorem le_supᵢ
deleted theorem le_supᵢ_iff
deleted theorem le_supᵢ_inf_supᵢ
deleted theorem le_supᵢ_of_le
deleted theorem le_supᵢ₂
deleted theorem le_supᵢ₂_of_le
deleted theorem le_supₛ
deleted theorem le_supₛ_iff
deleted theorem le_supₛ_of_le
added theorem lt_iInf_iff
added theorem lt_iSup_iff
deleted theorem lt_infᵢ_iff
added theorem lt_sSup_iff
deleted theorem lt_supᵢ_iff
deleted theorem lt_supₛ_iff
added theorem ofDual_iInf
added theorem ofDual_iSup
deleted theorem ofDual_infᵢ
deleted theorem ofDual_infₛ
added theorem ofDual_sInf
added theorem ofDual_sSup
deleted theorem ofDual_supᵢ
deleted theorem ofDual_supₛ
added theorem sInf_Prop_eq
added theorem sInf_apply
added theorem sInf_empty
added theorem sInf_eq_bot
added theorem sInf_eq_iInf'
added theorem sInf_eq_iInf
added theorem sInf_eq_top
added theorem sInf_image'
added theorem sInf_image2
added theorem sInf_image
added theorem sInf_insert
added theorem sInf_le
added theorem sInf_le_iff
added theorem sInf_le_of_le
added theorem sInf_le_sInf
added theorem sInf_le_sSup
added theorem sInf_lt_iff
added theorem sInf_pair
added theorem sInf_prod
added theorem sInf_range
added theorem sInf_singleton
added theorem sInf_sup_le_iInf_sup
added theorem sInf_union
added theorem sInf_univ
added theorem sSup_Prop_eq
added theorem sSup_apply
added theorem sSup_empty
added theorem sSup_eq_bot
added theorem sSup_eq_iSup'
added theorem sSup_eq_iSup
added theorem sSup_eq_top
added theorem sSup_image'
added theorem sSup_image2
added theorem sSup_image
added theorem sSup_insert
added theorem sSup_inter_le
added theorem sSup_le
added theorem sSup_le_iff
added theorem sSup_le_sSup
added theorem sSup_pair
added theorem sSup_prod
added theorem sSup_range
added theorem sSup_singleton
added theorem sSup_union
added theorem sSup_univ
added theorem sup_biSup
deleted theorem sup_bsupᵢ
added theorem sup_eq_iSup
deleted theorem sup_eq_supᵢ
added theorem sup_iSup
added theorem sup_iSup_nat_succ
deleted theorem sup_infₛ_le_infᵢ_sup
added theorem sup_sInf_le_iInf_sup
deleted theorem sup_supᵢ
deleted theorem sup_supᵢ_nat_succ
deleted def supᵢ.unexpander
deleted def supᵢ
deleted theorem supᵢ_Prop_eq
deleted theorem supᵢ_and'
deleted theorem supᵢ_and
deleted theorem supᵢ_apply
deleted theorem supᵢ_bool_eq
deleted theorem supᵢ_bot
deleted theorem supᵢ_comm
deleted theorem supᵢ_comp_le
deleted theorem supᵢ_congr
deleted theorem supᵢ_congr_Prop
deleted theorem supᵢ_const
deleted theorem supᵢ_const_le
deleted theorem supᵢ_const_mono
deleted theorem supᵢ_dite
deleted theorem supᵢ_emptyset
deleted theorem supᵢ_eq_bot
deleted theorem supᵢ_eq_dif
deleted theorem supᵢ_eq_if
deleted theorem supᵢ_eq_top
deleted theorem supᵢ_exists
deleted theorem supᵢ_extend_bot
deleted theorem supᵢ_false
deleted theorem supᵢ_image
deleted theorem supᵢ_inf_le_inf_supₛ
deleted theorem supᵢ_inf_le_supₛ_inf
deleted theorem supᵢ_infᵢ_ge_nat_add
deleted theorem supᵢ_insert
deleted theorem supᵢ_ite
deleted theorem supᵢ_le
deleted theorem supᵢ_le_iff
deleted theorem supᵢ_lt_iff
deleted theorem supᵢ_mono'
deleted theorem supᵢ_mono
deleted theorem supᵢ_nat_gt_zero_eq
deleted theorem supᵢ_ne_bot_subtype
deleted theorem supᵢ_neg
deleted theorem supᵢ_of_empty'
deleted theorem supᵢ_of_empty
deleted theorem supᵢ_option
deleted theorem supᵢ_option_elim
deleted theorem supᵢ_or
deleted theorem supᵢ_pair
deleted theorem supᵢ_plift_down
deleted theorem supᵢ_plift_up
deleted theorem supᵢ_pos
deleted theorem supᵢ_prod
deleted theorem supᵢ_range'
deleted theorem supᵢ_range
deleted theorem supᵢ_sigma
deleted theorem supᵢ_singleton
deleted theorem supᵢ_split
deleted theorem supᵢ_split_single
deleted theorem supᵢ_subtype''
deleted theorem supᵢ_subtype'
deleted theorem supᵢ_subtype
deleted theorem supᵢ_sum
deleted theorem supᵢ_sup
deleted theorem supᵢ_sup_eq
deleted theorem supᵢ_supᵢ_eq_left
deleted theorem supᵢ_supᵢ_eq_right
deleted theorem supᵢ_true
deleted theorem supᵢ_union
deleted theorem supᵢ_univ
deleted theorem supᵢ₂_comm
deleted theorem supᵢ₂_eq_bot
deleted theorem supᵢ₂_le
deleted theorem supᵢ₂_le_iff
deleted theorem supᵢ₂_le_supᵢ
deleted theorem supᵢ₂_mono'
deleted theorem supᵢ₂_mono
deleted theorem supₛ_Prop_eq
deleted theorem supₛ_apply
deleted theorem supₛ_diff_singleton_bot
deleted theorem supₛ_empty
deleted theorem supₛ_eq_bot
deleted theorem supₛ_eq_supᵢ'
deleted theorem supₛ_eq_supᵢ
deleted theorem supₛ_eq_top
deleted theorem supₛ_image'
deleted theorem supₛ_image2
deleted theorem supₛ_image
deleted theorem supₛ_insert
deleted theorem supₛ_inter_le
deleted theorem supₛ_le
deleted theorem supₛ_le_iff
deleted theorem supₛ_le_supₛ
deleted theorem supₛ_pair
deleted theorem supₛ_prod
deleted theorem supₛ_range
deleted theorem supₛ_singleton
deleted theorem supₛ_union
deleted theorem supₛ_univ
added theorem toDual_iInf
added theorem toDual_iSup
deleted theorem toDual_infᵢ
deleted theorem toDual_infₛ
added theorem toDual_sInf
added theorem toDual_sSup
deleted theorem toDual_supᵢ
deleted theorem toDual_supₛ
deleted theorem unary_relation_infₛ_iff
deleted theorem unary_relation_supₛ_iff
deleted theorem subset_infₛ_def
deleted theorem subset_infₛ_of_within
added theorem subset_sInf_def
added theorem subset_sInf_of_within
added theorem subset_sSup_def
added theorem subset_sSup_of_within
deleted theorem subset_supₛ_def
deleted theorem subset_supₛ_of_within
deleted theorem Concept.infₛ_fst
deleted theorem Concept.infₛ_snd
added theorem Concept.sInf_fst
added theorem Concept.sInf_snd
added theorem Concept.sSup_fst
added theorem Concept.sSup_snd
deleted theorem Concept.supₛ_fst
deleted theorem Concept.supₛ_snd
added theorem extentClosure_iUnion
deleted theorem extentClosure_unionᵢ
added theorem intentClosure_iUnion
deleted theorem intentClosure_unionᵢ
deleted theorem intentClosure_unionᵢ₂
added theorem IsGLB.ciInf_eq
added theorem IsGLB.ciInf_set_eq
deleted theorem IsGLB.cinfᵢ_eq
deleted theorem IsGLB.cinfᵢ_set_eq
deleted theorem IsGLB.cinfₛ_eq
added theorem IsGLB.csInf_eq
added theorem IsGreatest.csSup_eq
added theorem IsGreatest.csSup_mem
deleted theorem IsGreatest.csupₛ_eq
deleted theorem IsGreatest.csupₛ_mem
added theorem IsLUB.ciSup_eq
added theorem IsLUB.ciSup_set_eq
added theorem IsLUB.csSup_eq
deleted theorem IsLUB.csupᵢ_eq
deleted theorem IsLUB.csupᵢ_set_eq
deleted theorem IsLUB.csupₛ_eq
deleted theorem IsLeast.cinfₛ_eq
deleted theorem IsLeast.cinfₛ_mem
added theorem IsLeast.csInf_eq
added theorem IsLeast.csInf_mem
deleted theorem Monotone.cinfₛ_image_le
deleted theorem Monotone.csupₛ_image_le
deleted theorem Monotone.le_cinfₛ_image
deleted theorem Monotone.le_csupₛ_image
deleted theorem Monotone.map_cinfₛ
added theorem Monotone.map_csInf
deleted theorem MonotoneOn.map_cinfₛ
added theorem MonotoneOn.map_csInf
added theorem OrderIso.map_ciInf
added theorem OrderIso.map_ciInf_set
added theorem OrderIso.map_ciSup
added theorem OrderIso.map_ciSup_set
deleted theorem OrderIso.map_cinfᵢ
deleted theorem OrderIso.map_cinfᵢ_set
deleted theorem OrderIso.map_cinfₛ'
deleted theorem OrderIso.map_cinfₛ
added theorem OrderIso.map_csInf'
added theorem OrderIso.map_csInf
added theorem OrderIso.map_csSup'
added theorem OrderIso.map_csSup
deleted theorem OrderIso.map_csupᵢ
deleted theorem OrderIso.map_csupᵢ_set
deleted theorem OrderIso.map_csupₛ'
deleted theorem OrderIso.map_csupₛ
added theorem WithBot.ciSup_empty
added theorem WithBot.coe_iInf
added theorem WithBot.coe_iSup
deleted theorem WithBot.coe_infᵢ
deleted theorem WithBot.coe_infₛ'
added theorem WithBot.coe_sInf'
added theorem WithBot.coe_sSup'
deleted theorem WithBot.coe_supᵢ
deleted theorem WithBot.coe_supₛ'
added theorem WithBot.csSup_empty
deleted theorem WithBot.csupᵢ_empty
deleted theorem WithBot.csupₛ_empty
deleted theorem WithBot.infₛ_eq
added theorem WithBot.sInf_eq
added theorem WithBot.sSup_eq
deleted theorem WithBot.supₛ_eq
added theorem WithTop.coe_iInf
added theorem WithTop.coe_iSup
deleted theorem WithTop.coe_infᵢ
deleted theorem WithTop.coe_infₛ'
deleted theorem WithTop.coe_infₛ
added theorem WithTop.coe_sInf'
added theorem WithTop.coe_sInf
added theorem WithTop.coe_sSup'
added theorem WithTop.coe_sSup
deleted theorem WithTop.coe_supᵢ
deleted theorem WithTop.coe_supₛ'
deleted theorem WithTop.coe_supₛ
added theorem WithTop.iInf_empty
deleted theorem WithTop.infᵢ_empty
deleted theorem WithTop.infₛ_empty
deleted theorem WithTop.infₛ_eq
deleted theorem WithTop.isGLB_infₛ'
deleted theorem WithTop.isGLB_infₛ
added theorem WithTop.isGLB_sInf'
added theorem WithTop.isGLB_sInf
added theorem WithTop.isLUB_sSup'
added theorem WithTop.isLUB_sSup
deleted theorem WithTop.isLUB_supₛ'
deleted theorem WithTop.isLUB_supₛ
added theorem WithTop.sInf_empty
added theorem WithTop.sInf_eq
added theorem WithTop.sSup_eq
deleted theorem WithTop.supᵢ_coe_eq_top
deleted theorem WithTop.supᵢ_coe_lt_top
deleted theorem WithTop.supₛ_eq
added theorem ciInf_const
added theorem ciInf_le'
added theorem ciInf_le
added theorem ciInf_le_of_le
added theorem ciInf_mem
added theorem ciInf_mono
added theorem ciInf_pos
added theorem ciInf_set_le
added theorem ciInf_subsingleton
added theorem ciInf_unique
added theorem ciSup_const
added theorem ciSup_false
added theorem ciSup_le'
added theorem ciSup_le
added theorem ciSup_le_iff'
added theorem ciSup_le_iff
added theorem ciSup_mono'
added theorem ciSup_mono
added theorem ciSup_of_empty
added theorem ciSup_pos
added theorem ciSup_set_le_iff
added theorem ciSup_subsingleton
added theorem ciSup_unique
deleted theorem cinfᵢ_const
deleted theorem cinfᵢ_le'
deleted theorem cinfᵢ_le
deleted theorem cinfᵢ_le_of_le
deleted theorem cinfᵢ_mem
deleted theorem cinfᵢ_mono
deleted theorem cinfᵢ_pos
deleted theorem cinfᵢ_set_le
deleted theorem cinfᵢ_subsingleton
deleted theorem cinfᵢ_unique
deleted theorem cinfₛ_Icc
deleted theorem cinfₛ_Ici
deleted theorem cinfₛ_Ico
deleted theorem cinfₛ_Ioc
deleted theorem cinfₛ_Ioi
deleted theorem cinfₛ_Ioo
deleted theorem cinfₛ_insert
deleted theorem cinfₛ_le'
deleted theorem cinfₛ_le
deleted theorem cinfₛ_le_cinfₛ'
deleted theorem cinfₛ_le_cinfₛ
deleted theorem cinfₛ_le_csupₛ
deleted theorem cinfₛ_le_iff
deleted theorem cinfₛ_le_of_le
deleted theorem cinfₛ_lt_of_lt
deleted theorem cinfₛ_mem
deleted theorem cinfₛ_pair
deleted theorem cinfₛ_singleton
deleted theorem cinfₛ_union
deleted theorem cinfₛ_univ
added theorem csInf_Icc
added theorem csInf_Ici
added theorem csInf_Ico
added theorem csInf_Ioc
added theorem csInf_Ioi
added theorem csInf_Ioo
added theorem csInf_insert
added theorem csInf_le'
added theorem csInf_le
added theorem csInf_le_csInf'
added theorem csInf_le_csInf
added theorem csInf_le_csSup
added theorem csInf_le_iff
added theorem csInf_le_of_le
added theorem csInf_lt_of_lt
added theorem csInf_mem
added theorem csInf_pair
added theorem csInf_singleton
added theorem csInf_union
added theorem csInf_univ
added theorem csSup_Icc
added theorem csSup_Ico
added theorem csSup_Iic
added theorem csSup_Iio
added theorem csSup_Ioc
added theorem csSup_Ioo
added theorem csSup_empty
added theorem csSup_insert
added theorem csSup_inter_le
added theorem csSup_le'
added theorem csSup_le
added theorem csSup_le_csSup
added theorem csSup_le_iff'
added theorem csSup_le_iff
added theorem csSup_pair
added theorem csSup_singleton
added theorem csSup_union
deleted theorem csupᵢ_const
deleted theorem csupᵢ_false
deleted theorem csupᵢ_le'
deleted theorem csupᵢ_le
deleted theorem csupᵢ_le_iff'
deleted theorem csupᵢ_le_iff
deleted theorem csupᵢ_mono'
deleted theorem csupᵢ_mono
deleted theorem csupᵢ_of_empty
deleted theorem csupᵢ_pos
deleted theorem csupᵢ_set_le_iff
deleted theorem csupᵢ_subsingleton
deleted theorem csupᵢ_unique
deleted theorem csupₛ_Icc
deleted theorem csupₛ_Ico
deleted theorem csupₛ_Iic
deleted theorem csupₛ_Iio
deleted theorem csupₛ_Ioc
deleted theorem csupₛ_Ioo
deleted theorem csupₛ_empty
deleted theorem csupₛ_insert
deleted theorem csupₛ_inter_le
deleted theorem csupₛ_le'
deleted theorem csupₛ_le
deleted theorem csupₛ_le_csupₛ
deleted theorem csupₛ_le_iff'
deleted theorem csupₛ_le_iff
deleted theorem csupₛ_pair
deleted theorem csupₛ_singleton
deleted theorem csupₛ_union
added theorem exists_lt_of_ciInf_lt
deleted theorem exists_lt_of_cinfᵢ_lt
deleted theorem exists_lt_of_cinfₛ_lt
added theorem exists_lt_of_csInf_lt
added theorem exists_lt_of_lt_ciSup'
added theorem exists_lt_of_lt_ciSup
added theorem exists_lt_of_lt_csSup'
added theorem exists_lt_of_lt_csSup
deleted theorem exists_lt_of_lt_csupᵢ'
deleted theorem exists_lt_of_lt_csupᵢ
deleted theorem exists_lt_of_lt_csupₛ'
deleted theorem exists_lt_of_lt_csupₛ
deleted theorem infₛ_eq_argmin_on
added theorem isGLB_ciInf
added theorem isGLB_ciInf_set
deleted theorem isGLB_cinfᵢ
deleted theorem isGLB_cinfᵢ_set
deleted theorem isGLB_cinfₛ
added theorem isGLB_csInf
added theorem isLUB_ciSup
added theorem isLUB_ciSup_set
added theorem isLUB_csSup'
added theorem isLUB_csSup
deleted theorem isLUB_csupᵢ
deleted theorem isLUB_csupᵢ_set
deleted theorem isLUB_csupₛ'
deleted theorem isLUB_csupₛ
deleted theorem isLeast_cinfₛ
added theorem isLeast_csInf
added theorem le_ciInf
added theorem le_ciInf_iff'
added theorem le_ciInf_iff
added theorem le_ciInf_set_iff
added theorem le_ciSup
added theorem le_ciSup_iff'
added theorem le_ciSup_of_le
added theorem le_ciSup_set
deleted theorem le_cinfᵢ
deleted theorem le_cinfᵢ_iff'
deleted theorem le_cinfᵢ_iff
deleted theorem le_cinfᵢ_set_iff
deleted theorem le_cinfₛ
deleted theorem le_cinfₛ_iff''
deleted theorem le_cinfₛ_iff'
deleted theorem le_cinfₛ_iff
deleted theorem le_cinfₛ_inter
added theorem le_csInf
added theorem le_csInf_iff''
added theorem le_csInf_iff'
added theorem le_csInf_iff
added theorem le_csInf_inter
added theorem le_csSup
added theorem le_csSup_iff'
added theorem le_csSup_iff
added theorem le_csSup_of_le
deleted theorem le_csupᵢ
deleted theorem le_csupᵢ_iff'
deleted theorem le_csupᵢ_of_le
deleted theorem le_csupᵢ_set
deleted theorem le_csupₛ
deleted theorem le_csupₛ_iff'
deleted theorem le_csupₛ_iff
deleted theorem le_csupₛ_of_le
added theorem lt_csSup_of_lt
deleted theorem lt_csupₛ_of_lt
added theorem not_mem_of_csSup_lt
deleted theorem not_mem_of_csupₛ_lt
deleted theorem not_mem_of_lt_cinfₛ
added theorem not_mem_of_lt_csInf
added theorem sInf_eq_argmin_on
added theorem subset_Icc_csInf_csSup
modified theorem Finset.Nonempty.cInf_mem
modified theorem Finset.Nonempty.cSup_mem
deleted theorem Finset.inf'_id_eq_cinfₛ
deleted theorem Finset.sup'_id_eq_csupₛ
modified theorem Set.Finite.cSup_lt_iff
modified theorem Set.Finite.lt_cInf_iff
modified theorem Set.Nonempty.cInf_mem
modified theorem Set.Nonempty.cSup_mem
added theorem ciSup_mul_ciSup_le
added theorem ciSup_mul_le
deleted theorem csupᵢ_mul_csupᵢ_le
deleted theorem csupᵢ_mul_le
added theorem le_ciInf_mul
added theorem le_ciInf_mul_ciInf
deleted theorem le_cinfᵢ_mul
deleted theorem le_cinfᵢ_mul_cinfᵢ
added theorem le_mul_ciInf
deleted theorem le_mul_cinfᵢ
added theorem mul_ciSup_le
deleted theorem mul_csupᵢ_le
added theorem iSup_disjointed
added theorem iUnion_disjointed
deleted theorem supᵢ_disjointed
deleted theorem unionᵢ_disjointed
deleted theorem Filter.HasBasis.eq_infᵢ
added theorem Filter.hasBasis_iInf'
added theorem Filter.hasBasis_iInf
added theorem Filter.hasBasis_iSup
deleted theorem Filter.hasBasis_infᵢ'
deleted theorem Filter.hasBasis_infᵢ
deleted theorem Filter.hasBasis_supᵢ
added theorem Filter.biInf_sets_eq
added theorem Filter.biInter_mem
deleted theorem Filter.binfᵢ_sets_eq
deleted theorem Filter.binterᵢ_mem
added theorem Filter.comap_iInf
added theorem Filter.comap_iSup
deleted theorem Filter.comap_infᵢ
added theorem Filter.comap_sSup
deleted theorem Filter.comap_supᵢ
deleted theorem Filter.comap_supₛ
added theorem Filter.eventually_iSup
added theorem Filter.eventually_sSup
deleted theorem Filter.eventually_supᵢ
deleted theorem Filter.eventually_supₛ
added theorem Filter.frequently_iSup
added theorem Filter.frequently_sSup
deleted theorem Filter.frequently_supᵢ
deleted theorem Filter.frequently_supₛ
added theorem Filter.generate_iUnion
deleted theorem Filter.generate_unionᵢ
added theorem Filter.iInf_principal
added theorem Filter.iInf_sets_eq
added theorem Filter.iInter_mem
added theorem Filter.iSup_join
added theorem Filter.iSup_neBot
added theorem Filter.iSup_principal
added theorem Filter.iSup_sets_eq
deleted theorem Filter.infᵢ_eq_generate
deleted theorem Filter.infᵢ_principal
deleted theorem Filter.infᵢ_sets_eq
deleted theorem Filter.infᵢ_sets_induct
deleted theorem Filter.interᵢ_mem
deleted theorem Filter.interₛ_mem
added theorem Filter.map_biInf_eq
deleted theorem Filter.map_binfᵢ_eq
added theorem Filter.map_iInf_eq
added theorem Filter.map_iInf_le
added theorem Filter.map_iSup
deleted theorem Filter.map_infᵢ_eq
deleted theorem Filter.map_infᵢ_le
deleted theorem Filter.map_supᵢ
added theorem Filter.mem_iInf'
added theorem Filter.mem_iInf
added theorem Filter.mem_iInf_finite
added theorem Filter.mem_iInf_finset
added theorem Filter.mem_iInf_of_mem
added theorem Filter.mem_iSup
deleted theorem Filter.mem_infᵢ'
deleted theorem Filter.mem_infᵢ
deleted theorem Filter.mem_infᵢ_finite'
deleted theorem Filter.mem_infᵢ_finite
deleted theorem Filter.mem_infᵢ_finset
deleted theorem Filter.mem_infᵢ_of_mem
added theorem Filter.mem_sSup
deleted theorem Filter.mem_supᵢ
deleted theorem Filter.mem_supₛ
added theorem Filter.sInter_mem
added theorem Filter.sSup_sets_eq
deleted theorem Filter.supᵢ_join
deleted theorem Filter.supᵢ_neBot
deleted theorem Filter.supᵢ_principal
deleted theorem Filter.supᵢ_sets_eq
deleted theorem Filter.supₛ_sets_eq
added theorem Filter.tendsto_iInf'
added theorem Filter.tendsto_iInf
added theorem Filter.tendsto_iSup
deleted theorem Filter.tendsto_infᵢ'
deleted theorem Filter.tendsto_infᵢ
deleted theorem Filter.tendsto_supᵢ
added theorem countable_iInter_mem
deleted theorem countable_interᵢ_mem
deleted theorem countable_interₛ_mem
added theorem countable_sInter_mem
added theorem IsMaxOn.iSup_eq
deleted theorem IsMaxOn.supᵢ_eq
added theorem IsMinOn.iInf_eq
deleted theorem IsMinOn.infᵢ_eq
deleted theorem Filter.interₛ_lift_sets
added theorem Filter.lift'_iInf
deleted theorem Filter.lift'_infᵢ
added theorem Filter.lift_iInf
added theorem Filter.lift_iInf_le
deleted theorem Filter.lift_infᵢ
deleted theorem Filter.lift_infᵢ_le
modified theorem Filter.lift_mono'
added theorem Filter.prod_iInf_left
added theorem Filter.prod_iInf_right
deleted theorem Filter.prod_infᵢ_left
deleted theorem Filter.prod_infᵢ_right
added theorem Filter.smallSets_iInf
deleted theorem Filter.smallSets_infᵢ
deleted theorem GaloisConnection.l_supᵢ
deleted theorem GaloisConnection.l_supₛ
deleted theorem GaloisConnection.u_infᵢ
deleted theorem GaloisConnection.u_infₛ
deleted theorem InfₛHom.cancel_left
deleted theorem InfₛHom.cancel_right
deleted theorem InfₛHom.coe_comp
deleted theorem InfₛHom.coe_copy
deleted theorem InfₛHom.coe_id
deleted theorem InfₛHom.coe_top
deleted def InfₛHom.comp
deleted theorem InfₛHom.comp_apply
deleted theorem InfₛHom.comp_assoc
deleted theorem InfₛHom.comp_id
deleted theorem InfₛHom.copy_eq
deleted theorem InfₛHom.dual_comp
deleted theorem InfₛHom.dual_id
deleted theorem InfₛHom.ext
deleted theorem InfₛHom.id_apply
deleted theorem InfₛHom.id_comp
deleted theorem InfₛHom.symm_dual_comp
deleted theorem InfₛHom.symm_dual_id
deleted theorem InfₛHom.toFun_eq_coe
deleted theorem InfₛHom.top_apply
deleted structure InfₛHom
added theorem Set.image_sSup
deleted theorem Set.image_supₛ
deleted theorem SupₛHom.bot_apply
deleted theorem SupₛHom.cancel_left
deleted theorem SupₛHom.cancel_right
deleted theorem SupₛHom.coe_bot
deleted theorem SupₛHom.coe_comp
deleted theorem SupₛHom.coe_copy
deleted theorem SupₛHom.coe_id
deleted def SupₛHom.comp
deleted theorem SupₛHom.comp_apply
deleted theorem SupₛHom.comp_assoc
deleted theorem SupₛHom.comp_id
deleted theorem SupₛHom.copy_eq
deleted theorem SupₛHom.dual_comp
deleted theorem SupₛHom.dual_id
deleted theorem SupₛHom.ext
deleted theorem SupₛHom.id_apply
deleted theorem SupₛHom.id_comp
deleted def SupₛHom.setImage
deleted theorem SupₛHom.symm_dual_comp
deleted theorem SupₛHom.symm_dual_id
deleted theorem SupₛHom.toFun_eq_coe
deleted structure SupₛHom
deleted def infInfₛHom
deleted theorem infInfₛHom_apply
added def infsInfHom
added theorem infsInfHom_apply
added theorem map_iInf
added theorem map_iInf₂
added theorem map_iSup
added theorem map_iSup₂
deleted theorem map_infᵢ
deleted theorem map_infᵢ₂
deleted theorem map_supᵢ
deleted theorem map_supᵢ₂
added theorem sInfHom.cancel_left
added theorem sInfHom.cancel_right
added theorem sInfHom.coe_comp
added theorem sInfHom.coe_copy
added theorem sInfHom.coe_id
added theorem sInfHom.coe_top
added def sInfHom.comp
added theorem sInfHom.comp_apply
added theorem sInfHom.comp_assoc
added theorem sInfHom.comp_id
added theorem sInfHom.copy_eq
added theorem sInfHom.dual_comp
added theorem sInfHom.dual_id
added theorem sInfHom.ext
added theorem sInfHom.id_apply
added theorem sInfHom.id_comp
added theorem sInfHom.symm_dual_comp
added theorem sInfHom.symm_dual_id
added theorem sInfHom.toFun_eq_coe
added theorem sInfHom.top_apply
added structure sInfHom
added theorem sSupHom.bot_apply
added theorem sSupHom.cancel_left
added theorem sSupHom.cancel_right
added theorem sSupHom.coe_bot
added theorem sSupHom.coe_comp
added theorem sSupHom.coe_copy
added theorem sSupHom.coe_id
added def sSupHom.comp
added theorem sSupHom.comp_apply
added theorem sSupHom.comp_assoc
added theorem sSupHom.comp_id
added theorem sSupHom.copy_eq
added theorem sSupHom.dual_comp
added theorem sSupHom.dual_id
added theorem sSupHom.ext
added theorem sSupHom.id_apply
added theorem sSupHom.id_comp
added def sSupHom.setImage
added theorem sSupHom.symm_dual_comp
added theorem sSupHom.symm_dual_id
added theorem sSupHom.toFun_eq_coe
added structure sSupHom
deleted def supSupₛHom
deleted theorem supSupₛHom_apply
added def supsSupHom
added theorem supsSupHom_apply
added theorem OrderHom.coe_iInf
added theorem OrderHom.coe_iSup
deleted theorem OrderHom.coe_infᵢ
deleted theorem OrderHom.coe_supᵢ
added theorem OrderHom.iInf_apply
added theorem OrderHom.iSup_apply
deleted theorem OrderHom.infᵢ_apply
deleted theorem OrderHom.infₛ_apply
added theorem OrderHom.sInf_apply
added theorem OrderHom.sSup_apply
deleted theorem OrderHom.supᵢ_apply
deleted theorem OrderHom.supₛ_apply
deleted theorem Order.Ideal.coe_infₛ
added theorem Order.Ideal.coe_sInf
deleted theorem Order.Ideal.mem_infₛ
added theorem Order.Ideal.mem_sInf
modified theorem Filter.bliminf_eq
modified theorem Filter.blimsup_eq
added theorem Filter.iInf_le_liminf
deleted theorem Filter.infᵢ_le_liminf
deleted theorem Filter.le_liminfₛ_of_le
deleted theorem Filter.le_limsupₛ_of_le
modified theorem Filter.liminf_eq
deleted def Filter.liminfₛ
deleted theorem Filter.liminfₛ_bot
deleted theorem Filter.liminfₛ_le_of_le
deleted theorem Filter.liminfₛ_top
added def Filter.limsInf
added theorem Filter.limsInf_bot
added theorem Filter.limsInf_top
added def Filter.limsSup
added theorem Filter.limsSup_bot
added theorem Filter.limsSup_top
modified theorem Filter.limsup_eq
added theorem Filter.limsup_le_iSup
deleted theorem Filter.limsup_le_supᵢ
deleted def Filter.limsupₛ
deleted theorem Filter.limsupₛ_bot
deleted theorem Filter.limsupₛ_le_of_le
deleted theorem Filter.limsupₛ_top
deleted theorem Order.PFilter.infₛ_gc
added theorem Order.PFilter.sInf_gc
added theorem ciSup_partialSups_eq
deleted theorem csupᵢ_partialSups_eq
added theorem iSup_partialSups_eq
added theorem partialSups_eq_biSup
deleted theorem partialSups_eq_bsupᵢ
deleted theorem supᵢ_partialSups_eq
added theorem Order.pred_eq_iSup
deleted theorem Order.pred_eq_supᵢ
added theorem Order.succ_eq_iInf
deleted theorem Order.succ_eq_infᵢ
deleted theorem Finset.SupIndep.bunionᵢ
added theorem LowerSet.Iic_iInf
added theorem LowerSet.Iic_iInf₂
deleted theorem LowerSet.Iic_infᵢ
deleted theorem LowerSet.Iic_infᵢ₂
deleted theorem LowerSet.Iic_infₛ
added theorem LowerSet.Iic_sInf
added theorem LowerSet.coe_iInf
added theorem LowerSet.coe_iInf₂
added theorem LowerSet.coe_iSup
added theorem LowerSet.coe_iSup₂
deleted theorem LowerSet.coe_infᵢ
deleted theorem LowerSet.coe_infᵢ₂
deleted theorem LowerSet.coe_infₛ
added theorem LowerSet.coe_sInf
added theorem LowerSet.coe_sSup
deleted theorem LowerSet.coe_supᵢ
deleted theorem LowerSet.coe_supᵢ₂
deleted theorem LowerSet.coe_supₛ
added theorem LowerSet.compl_iInf₂
added theorem LowerSet.compl_iSup₂
deleted theorem LowerSet.compl_infᵢ₂
deleted theorem LowerSet.compl_supᵢ₂
added theorem LowerSet.iSup_Iic
added theorem LowerSet.mem_iInf_iff
added theorem LowerSet.mem_iSup_iff
deleted theorem LowerSet.mem_infᵢ_iff
deleted theorem LowerSet.mem_infₛ_iff
added theorem LowerSet.mem_sInf_iff
added theorem LowerSet.mem_sSup_iff
deleted theorem LowerSet.mem_supᵢ_iff
deleted theorem LowerSet.mem_supₛ_iff
deleted theorem LowerSet.supᵢ_Iic
added theorem UpperSet.Ici_iSup
added theorem UpperSet.Ici_iSup₂
added theorem UpperSet.Ici_sSup
deleted theorem UpperSet.Ici_supᵢ
deleted theorem UpperSet.Ici_supᵢ₂
deleted theorem UpperSet.Ici_supₛ
added theorem UpperSet.coe_iInf
added theorem UpperSet.coe_iInf₂
added theorem UpperSet.coe_iSup
added theorem UpperSet.coe_iSup₂
deleted theorem UpperSet.coe_infᵢ
deleted theorem UpperSet.coe_infᵢ₂
deleted theorem UpperSet.coe_infₛ
added theorem UpperSet.coe_sInf
added theorem UpperSet.coe_sSup
deleted theorem UpperSet.coe_supᵢ
deleted theorem UpperSet.coe_supᵢ₂
deleted theorem UpperSet.coe_supₛ
added theorem UpperSet.compl_iInf₂
added theorem UpperSet.compl_iSup₂
deleted theorem UpperSet.compl_infᵢ₂
deleted theorem UpperSet.compl_supᵢ₂
added theorem UpperSet.iInf_Ici
deleted theorem UpperSet.infᵢ_Ici
added theorem UpperSet.mem_iInf_iff
added theorem UpperSet.mem_iSup_iff
deleted theorem UpperSet.mem_infᵢ_iff
deleted theorem UpperSet.mem_infₛ_iff
added theorem UpperSet.mem_sInf_iff
added theorem UpperSet.mem_sSup_iff
deleted theorem UpperSet.mem_supᵢ_iff
deleted theorem UpperSet.mem_supₛ_iff
added theorem isLowerSet_iInter
added theorem isLowerSet_iInter₂
added theorem isLowerSet_iUnion
added theorem isLowerSet_iUnion₂
deleted theorem isLowerSet_interᵢ
deleted theorem isLowerSet_interᵢ₂
deleted theorem isLowerSet_interₛ
added theorem isLowerSet_sInter
added theorem isLowerSet_sUnion
deleted theorem isLowerSet_unionᵢ
deleted theorem isLowerSet_unionᵢ₂
deleted theorem isLowerSet_unionₛ
added theorem isUpperSet_iInter
added theorem isUpperSet_iInter₂
added theorem isUpperSet_iUnion
added theorem isUpperSet_iUnion₂
deleted theorem isUpperSet_interᵢ
deleted theorem isUpperSet_interᵢ₂
deleted theorem isUpperSet_interₛ
added theorem isUpperSet_sInter
added theorem isUpperSet_sUnion
deleted theorem isUpperSet_unionᵢ
deleted theorem isUpperSet_unionᵢ₂
deleted theorem isUpperSet_unionₛ
added theorem lowerClosure_iUnion
added theorem lowerClosure_sUnion
deleted theorem lowerClosure_unionᵢ
deleted theorem lowerClosure_unionₛ
added theorem upperClosure_iUnion
added theorem upperClosure_sUnion
deleted theorem upperClosure_unionᵢ
deleted theorem upperClosure_unionₛ
deleted theorem LowerSet.coe_iicInfₛHom
deleted theorem UpperSet.coe_iciSupₛHom
deleted theorem Algebra.adjoin_eq_infₛ
added theorem Algebra.adjoin_eq_sInf
added theorem Algebra.adjoin_iUnion
deleted theorem Algebra.adjoin_unionᵢ
added theorem Submodule.fg_biSup
deleted theorem Submodule.fg_bsupᵢ
added theorem Submodule.fg_iSup
deleted theorem Submodule.fg_supᵢ
added theorem Ideal.mem_iInf
added theorem Ideal.mem_iSup_of_mem
deleted theorem Ideal.mem_infᵢ
deleted theorem Ideal.mem_infₛ
added theorem Ideal.mem_sInf
added theorem Ideal.mem_sSup_of_mem
deleted theorem Ideal.mem_supᵢ_of_mem
deleted theorem Ideal.mem_supₛ_of_mem
added theorem Ideal.span_iUnion
deleted theorem Ideal.span_unionᵢ
added theorem Ideal.comap_iInf
deleted theorem Ideal.comap_infᵢ
deleted theorem Ideal.comap_infₛ'
deleted theorem Ideal.comap_infₛ
added theorem Ideal.comap_sInf'
added theorem Ideal.comap_sInf
added theorem Ideal.iInf_sup_eq_top
deleted theorem Ideal.infᵢ_sup_eq_top
added theorem Ideal.map_iSup
deleted theorem Ideal.map_infₛ
added theorem Ideal.map_sInf
added theorem Ideal.map_sSup
deleted theorem Ideal.map_supᵢ
deleted theorem Ideal.map_supₛ
deleted theorem Ideal.radical_eq_infₛ
added theorem Ideal.radical_eq_sInf
added theorem Ideal.sup_iInf_eq_top
deleted theorem Ideal.sup_infᵢ_eq_top
added theorem Submodule.smul_iInf_le
added theorem Submodule.smul_iSup
deleted theorem Submodule.smul_infᵢ_le
deleted theorem Submodule.smul_supᵢ
deleted theorem nilradical_eq_infₛ
added theorem nilradical_eq_sInf
added theorem Subring.closure_iUnion
added theorem Subring.closure_sUnion
deleted theorem Subring.closure_unionᵢ
deleted theorem Subring.closure_unionₛ
added theorem Subring.coe_iInf
deleted theorem Subring.coe_infᵢ
deleted theorem Subring.coe_infₛ
added theorem Subring.coe_sInf
added theorem Subring.comap_iInf
deleted theorem Subring.comap_infᵢ
added theorem Subring.map_iSup
deleted theorem Subring.map_supᵢ
added theorem Subring.mem_iInf
deleted theorem Subring.mem_infᵢ
deleted theorem Subring.mem_infₛ
added theorem Subring.mem_sInf
deleted theorem Subsemiring.coe_infₛ
added theorem Subsemiring.coe_sInf
added theorem Subsemiring.comap_iInf
deleted theorem Subsemiring.comap_infᵢ
added theorem Subsemiring.map_iSup
deleted theorem Subsemiring.map_supᵢ
deleted theorem Subsemiring.mem_infₛ
added theorem Subsemiring.mem_sInf
added theorem Cardinal.iSup_le_sum
deleted theorem Cardinal.infₛ_empty
added theorem Cardinal.lift_iInf
added theorem Cardinal.lift_iSup
added theorem Cardinal.lift_iSup_le
deleted theorem Cardinal.lift_infᵢ
deleted theorem Cardinal.lift_infₛ
added theorem Cardinal.lift_sInf
added theorem Cardinal.lift_sSup
deleted theorem Cardinal.lift_supᵢ
deleted theorem Cardinal.lift_supᵢ_le
deleted theorem Cardinal.lift_supₛ
added theorem Cardinal.mk_biUnion_le
deleted theorem Cardinal.mk_bunionᵢ_le
added theorem Cardinal.mk_iUnion_le
added theorem Cardinal.mk_sUnion_le
deleted theorem Cardinal.mk_unionᵢ_le
deleted theorem Cardinal.mk_unionₛ_le
added theorem Cardinal.sInf_empty
modified theorem Cardinal.succ_def
added theorem Cardinal.sum_le_iSup
deleted theorem Cardinal.sum_le_supᵢ
deleted theorem Cardinal.supᵢ_le_sum
added theorem Ordinal.iSup_lt
added theorem Ordinal.iSup_lt_lift
deleted theorem Ordinal.supᵢ_lt
deleted theorem Ordinal.supᵢ_lt_lift
modified theorem Ordinal.div_def
modified theorem Ordinal.enumOrd_def
modified theorem Ordinal.enumOrd_zero
added theorem Ordinal.iSup_ord
added theorem Ordinal.sSup_eq_bsup
added theorem Ordinal.sSup_eq_sup
added theorem Ordinal.sSup_ord
added theorem Ordinal.sup_eq_sSup
deleted theorem Ordinal.sup_eq_supₛ
deleted theorem Ordinal.supᵢ_ord
deleted theorem Ordinal.supₛ_eq_bsup
deleted theorem Ordinal.supₛ_eq_sup
deleted theorem Ordinal.supₛ_ord
deleted theorem Ordinal.infₛ_empty
added theorem Ordinal.sInf_empty
modified theorem Ordinal.log_def
deleted theorem Class.coe_interₛ
added theorem Class.coe_sInter
added theorem Class.coe_sUnion
deleted theorem Class.coe_unionₛ
deleted def Class.interₛ
deleted theorem Class.interₛ_apply
deleted theorem Class.interₛ_empty
deleted theorem Class.mem_interₛ
deleted theorem Class.mem_of_mem_interₛ
added theorem Class.mem_sInter
added theorem Class.mem_sUnion
deleted theorem Class.mem_unionₛ
added def Class.sInter
added theorem Class.sInter_apply
added theorem Class.sInter_empty
added def Class.sUnion
added theorem Class.sUnion_apply
added theorem Class.sUnion_empty
deleted def Class.unionₛ
deleted theorem Class.unionₛ_apply
deleted theorem Class.unionₛ_empty
added theorem PSet.mem_sUnion
deleted theorem PSet.mem_unionₛ
added def PSet.sUnion
added theorem PSet.toSet_sUnion
deleted theorem PSet.toSet_unionₛ
deleted def PSet.unionₛ
deleted theorem ZFSet.interₛ_empty
deleted theorem ZFSet.interₛ_singleton
deleted theorem ZFSet.mem_interₛ
deleted theorem ZFSet.mem_of_mem_interₛ
added theorem ZFSet.mem_sInter
added theorem ZFSet.mem_sUnion
deleted theorem ZFSet.mem_unionₛ
deleted theorem ZFSet.mem_unionₛ_of_mem
added theorem ZFSet.sInter_empty
added theorem ZFSet.sInter_singleton
added def ZFSet.sUnion
added theorem ZFSet.sUnion_empty
added theorem ZFSet.sUnion_lem
added theorem ZFSet.sUnion_pair
added theorem ZFSet.sUnion_singleton
deleted theorem ZFSet.toSet_interₛ
added theorem ZFSet.toSet_sInter
added theorem ZFSet.toSet_sUnion
deleted theorem ZFSet.toSet_unionₛ
deleted def ZFSet.unionₛ
deleted theorem ZFSet.unionₛ_empty
deleted theorem ZFSet.unionₛ_lem
deleted theorem ZFSet.unionₛ_pair
deleted theorem ZFSet.unionₛ_singleton
added theorem continuousInv_iInf
deleted theorem continuousInv_infᵢ
deleted theorem continuousInv_infₛ
added theorem continuousInv_sInf
added theorem topologicalGroup_iInf
deleted theorem topologicalGroup_infᵢ
deleted theorem topologicalGroup_infₛ
added theorem topologicalGroup_sInf
added theorem rel_iSup_sum
added theorem rel_iSup_tsum
deleted theorem rel_supᵢ_sum
deleted theorem rel_supᵢ_tsum
added theorem tsum_iSup_decode₂
added theorem tsum_iUnion_decode₂
deleted theorem tsum_supᵢ_decode₂
deleted theorem tsum_unionᵢ_decode₂
added theorem continuousMul_iInf
deleted theorem continuousMul_infᵢ
deleted theorem continuousMul_infₛ
added theorem continuousMul_sInf
added theorem continuousSMul_iInf
deleted theorem continuousSMul_infᵢ
deleted theorem continuousSMul_infₛ
added theorem continuousSMul_sInf
deleted theorem IsCompact.infₛ_mem
deleted theorem IsCompact.isGLB_infₛ
added theorem IsCompact.isGLB_sInf
added theorem IsCompact.isLUB_sSup
deleted theorem IsCompact.isLUB_supₛ
deleted theorem IsCompact.isLeast_infₛ
added theorem IsCompact.isLeast_sInf
added theorem IsCompact.sInf_mem
added theorem IsCompact.sSup_mem
deleted theorem IsCompact.supₛ_mem
deleted theorem liminfₛ_eq_of_le_nhds
deleted theorem liminfₛ_nhds
added theorem limsInf_eq_of_le_nhds
added theorem limsInf_nhds
added theorem limsSup_eq_of_le_nhds
added theorem limsSup_nhds
deleted theorem limsupₛ_eq_of_le_nhds
deleted theorem limsupₛ_nhds
added theorem iInf_eq_of_tendsto
added theorem iSup_eq_of_tendsto
deleted theorem infᵢ_eq_of_tendsto
deleted theorem supᵢ_eq_of_tendsto
added theorem tendsto_atBot_ciInf
added theorem tendsto_atBot_ciSup
deleted theorem tendsto_atBot_cinfᵢ
deleted theorem tendsto_atBot_csupᵢ
added theorem tendsto_atBot_iInf
added theorem tendsto_atBot_iSup
deleted theorem tendsto_atBot_infᵢ
deleted theorem tendsto_atBot_supᵢ
added theorem tendsto_atTop_ciInf
added theorem tendsto_atTop_ciSup
deleted theorem tendsto_atTop_cinfᵢ
deleted theorem tendsto_atTop_csupᵢ
added theorem tendsto_atTop_iInf
added theorem tendsto_atTop_iSup
deleted theorem tendsto_atTop_infᵢ
deleted theorem tendsto_atTop_supᵢ
added theorem uniformGroup_iInf
deleted theorem uniformGroup_infᵢ
deleted theorem uniformGroup_infₛ
added theorem uniformGroup_sInf
deleted theorem isTopologicalBasis_infᵢ
added theorem Finset.closure_biUnion
deleted theorem Finset.closure_bunionᵢ
added theorem Finset.interior_iInter
deleted theorem Finset.interior_interᵢ
added theorem closure_iUnion
deleted theorem closure_unionᵢ
added theorem interior_iInter
added theorem interior_iInter_subset
deleted theorem interior_interᵢ
deleted theorem interior_interᵢ_subset
deleted theorem interior_interₛ_subset
added theorem interior_sInter_subset
added theorem isClosed_biInter
added theorem isClosed_biUnion
deleted theorem isClosed_binterᵢ
deleted theorem isClosed_bunionᵢ
added theorem isClosed_iInter
added theorem isClosed_iUnion
deleted theorem isClosed_interᵢ
deleted theorem isClosed_interₛ
added theorem isClosed_sInter
deleted theorem isClosed_unionᵢ
added theorem isOpen_biInter
added theorem isOpen_biInter_finset
added theorem isOpen_biUnion
deleted theorem isOpen_binterᵢ
deleted theorem isOpen_binterᵢ_finset
deleted theorem isOpen_bunionᵢ
added theorem isOpen_iInter
added theorem isOpen_iUnion
deleted theorem isOpen_interᵢ
deleted theorem isOpen_interₛ
added theorem isOpen_sInter
added theorem isOpen_sUnion
deleted theorem isOpen_unionᵢ
deleted theorem isOpen_unionₛ
added theorem isPreconnected_iUnion
added theorem isPreconnected_sUnion
deleted theorem isPreconnected_unionᵢ
deleted theorem isPreconnected_unionₛ
deleted theorem continuous_infₛ_dom₂
added theorem continuous_sInf_dom₂
added theorem inducing_iInf_to_pi
deleted theorem inducing_infᵢ_to_pi
added theorem nhdsWithin_biUnion
deleted theorem nhdsWithin_bunionᵢ
added theorem nhdsWithin_iUnion
added theorem nhdsWithin_sUnion
deleted theorem nhdsWithin_unionᵢ
deleted theorem nhdsWithin_unionₛ
deleted theorem Filter.interₛ_nhds
added theorem Filter.nhds_iInf
deleted theorem Filter.nhds_infᵢ
added theorem Filter.sInter_nhds
added theorem isGδ_biInter
added theorem isGδ_biInter_of_open
added theorem isGδ_biUnion
deleted theorem isGδ_binterᵢ
deleted theorem isGδ_binterᵢ_of_open
deleted theorem isGδ_bunionᵢ
added theorem isGδ_iInter
added theorem isGδ_iInter_of_open
deleted theorem isGδ_interᵢ
deleted theorem isGδ_interᵢ_of_open
deleted theorem isGδ_interₛ
added theorem isGδ_sInter
added theorem ENNReal.add_biSup'
added theorem ENNReal.add_biSup
deleted theorem ENNReal.add_bsupᵢ'
deleted theorem ENNReal.add_bsupᵢ
added theorem ENNReal.add_iSup
deleted theorem ENNReal.add_supᵢ
added theorem ENNReal.biInf_le_nhds
added theorem ENNReal.biSup_add'
added theorem ENNReal.biSup_add
deleted theorem ENNReal.binfᵢ_le_nhds
deleted theorem ENNReal.bsupᵢ_add'
deleted theorem ENNReal.bsupᵢ_add
added theorem ENNReal.iInf_mul_left'
added theorem ENNReal.iInf_mul_left
added theorem ENNReal.iInf_mul_right
added theorem ENNReal.iSup_add
added theorem ENNReal.iSup_add_iSup
added theorem ENNReal.iSup_div
added theorem ENNReal.iSup_mul
deleted theorem ENNReal.infᵢ_mul_left'
deleted theorem ENNReal.infᵢ_mul_left
deleted theorem ENNReal.infᵢ_mul_right'
deleted theorem ENNReal.infᵢ_mul_right
added theorem ENNReal.inv_map_iInf
added theorem ENNReal.inv_map_iSup
deleted theorem ENNReal.inv_map_infᵢ
deleted theorem ENNReal.inv_map_supᵢ
added theorem ENNReal.mul_iSup
added theorem ENNReal.mul_sSup
deleted theorem ENNReal.mul_supᵢ
deleted theorem ENNReal.mul_supₛ
added theorem ENNReal.sSup_add
added theorem ENNReal.sub_iSup
deleted theorem ENNReal.sub_supᵢ
deleted theorem ENNReal.supᵢ_add
deleted theorem ENNReal.supᵢ_add_supᵢ
deleted theorem ENNReal.supᵢ_div
deleted theorem ENNReal.supᵢ_mul
deleted theorem ENNReal.supₛ_add
deleted theorem ENNReal.tsum_bunionᵢ_le
added theorem ENNReal.tsum_iSup_eq
added theorem ENNReal.tsum_iUnion_le
deleted theorem ENNReal.tsum_supᵢ_eq
deleted theorem ENNReal.tsum_unionᵢ_le
modified theorem Real.diam_eq
modified theorem EReal.nhds_top'
added theorem dense_biInter_of_Gδ
added theorem dense_biInter_of_open
deleted theorem dense_binterᵢ_of_Gδ
deleted theorem dense_binterᵢ_of_open
added theorem dense_iInter_of_Gδ
added theorem dense_iInter_of_open
deleted theorem dense_interᵢ_of_Gδ
deleted theorem dense_interᵢ_of_open
deleted theorem dense_interₛ_of_Gδ
deleted theorem dense_interₛ_of_open
added theorem dense_sInter_of_Gδ
added theorem dense_sInter_of_open
added theorem Metric.bounded_biUnion
deleted theorem Metric.bounded_bunionᵢ
added theorem Metric.iUnion_ball_nat
deleted theorem Metric.unionᵢ_ball_nat
added theorem EMetric.diam_eq_sSup
deleted theorem EMetric.diam_eq_supₛ
deleted theorem EMetric.infEdist_unionᵢ
added theorem Metric.infDist_eq_iInf
deleted theorem Metric.infDist_eq_infᵢ
added theorem Set.einfsep_eq_iInf
deleted theorem Set.einfsep_eq_infᵢ
added theorem Set.infsep_eq_iInf
deleted theorem Set.infsep_eq_infᵢ
added theorem Scott.isOpen_sUnion
deleted theorem Scott.isOpen_unionₛ
added theorem coinduced_iSup
deleted theorem coinduced_supᵢ
added theorem continuous_iInf_dom
added theorem continuous_iInf_rng
added theorem continuous_iSup_dom
added theorem continuous_iSup_rng
deleted theorem continuous_infᵢ_dom
deleted theorem continuous_infᵢ_rng
deleted theorem continuous_infₛ_dom
deleted theorem continuous_infₛ_rng
added theorem continuous_sInf_dom
added theorem continuous_sInf_rng
added theorem continuous_sSup_dom
added theorem continuous_sSup_rng
deleted theorem continuous_supᵢ_dom
deleted theorem continuous_supᵢ_rng
deleted theorem continuous_supₛ_dom
deleted theorem continuous_supₛ_rng
added theorem generateFrom_iInter
added theorem generateFrom_iUnion
deleted theorem generateFrom_interᵢ
added theorem generateFrom_sUnion
deleted theorem generateFrom_unionᵢ
deleted theorem generateFrom_unionₛ
added theorem induced_iInf
deleted theorem induced_infᵢ
added theorem isClosed_iSup_iff
deleted theorem isClosed_supᵢ_iff
added theorem isOpen_iSup_iff
deleted theorem isOpen_supᵢ_iff
added theorem nhds_iInf
deleted theorem nhds_infᵢ
deleted theorem nhds_infₛ
added theorem nhds_sInf
added theorem setOf_isOpen_iSup
added theorem setOf_isOpen_sSup
deleted theorem setOf_isOpen_supᵢ
deleted theorem setOf_isOpen_supₛ
added theorem Dense.Iio_eq_biUnion
deleted theorem Dense.Iio_eq_bunionᵢ
added theorem Dense.Ioi_eq_biUnion
deleted theorem Dense.Ioi_eq_bunionᵢ
deleted theorem IsClosed.cinfₛ_mem
added theorem IsClosed.csInf_mem
added theorem IsClosed.csSup_mem
deleted theorem IsClosed.csupₛ_mem
deleted theorem IsClosed.infₛ_mem
added theorem IsClosed.sInf_mem
added theorem IsClosed.sSup_mem
deleted theorem IsClosed.supₛ_mem
deleted theorem cinfₛ_mem_closure
added theorem csInf_mem_closure
added theorem csSup_mem_closure
deleted theorem csupₛ_mem_closure
deleted theorem exists_seq_tendsto_infₛ
deleted theorem exists_seq_tendsto_supₛ
deleted theorem infₛ_mem_closure
added theorem nhds_eq_iInf_abs_sub
deleted theorem nhds_eq_infᵢ_abs_sub
added theorem sInf_mem_closure
added theorem sSup_mem_closure
deleted theorem supₛ_mem_closure
added theorem biInter_basis_nhds
deleted theorem binterᵢ_basis_nhds
added theorem regularSpace_iInf
deleted theorem regularSpace_infᵢ
deleted theorem regularSpace_infₛ
added theorem regularSpace_sInf
added theorem iUnion_compactCovering
added theorem isClopen_biInter
added theorem isClopen_biUnion
deleted theorem isClopen_binterᵢ
deleted theorem isClopen_binterᵢ_finset
deleted theorem isClopen_bunionᵢ
deleted theorem isClopen_bunionᵢ_finset
added theorem isClopen_iInter
added theorem isClopen_iUnion
deleted theorem isClopen_interᵢ
deleted theorem isClopen_unionᵢ
added theorem isCompact_iUnion
deleted theorem isCompact_unionᵢ
deleted theorem unionᵢ_compactCovering
deleted theorem UniformSpace.comap_infᵢ
added theorem iInf_uniformity
deleted theorem infᵢ_uniformity
deleted theorem supᵢ_nhds_le_uniformity
deleted theorem toTopologicalSpace_infᵢ
deleted theorem toTopologicalSpace_infₛ