Mathlib Map

Theorems · Theorem · order theory

iSup_congr

∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] {f g : ι → α}, (∀ (i : ι), f i = g i) → ⨆ i, f i = ⨆ i, g i
Defined in
Mathlib.Order.CompleteLattice.Basic
Cited by
15 results in Mathlib
Foundations
Depth 5 from the axioms · uses Quot.sound
Assumes
SupSet
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

biSup_prod · cited by 5biSup_prodSet.iUnion_congr · cited by 5Set.iUnion_congrbiSup_congr · cited by 4biSup_congrProbabilityTheory.Kernel.indep_iSup_limsup · cited by 3Kernel.indep_iSup_limsupSubmodule.map₂_map_right · cited by 2Submodule.map₂_map_rightSubmodule.map_map₂ · cited by 2Submodule.map_map₂MeasureTheory.OuterMeasure.trim_iSup · cited by 1OuterMeasure.trim_iSupIsUltrametricDist.isPowMul_invariantExtension · cited by 1IsUltrametricDist.isPowMu…AEMeasurable.biSup · cited by 1AEMeasurable.biSupAlgebraicGeometry.Scheme.Modules.exists_isOpenCover_presentation · cited by 1Modules.exists_isOpenCove…spectralNorm_unique_of_finiteDimensional_normal · cited by 0spectralNorm_unique_of_fi…MeasureTheory.Measure.OuterRegular.ext_isOpen_isBounded · cited by 0OuterRegular.ext_isOpen_i…IntermediateField.isSplittingField_iSup · cited by 0IntermediateField.isSplit…MeasureTheory.addContent_iUnion_eq_tsum_of_addContent_iUnion_eq_iSup · cited by 0MeasureTheory.addContent_…HahnEmbedding.ArchimedeanStrata.isInternal_stratum' · cited by 0ArchimedeanStrata.isInter…iSup · cited by 2415iSupSupSet · cited by 154SupSetiSup_congrCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • iSupstatement and proof · cited by 2,415
  • SupSetstatement and proof · cited by 154

Cited by15

Results whose statement or proof uses this declaration.