Mathlib Map

Theorems · Theorem · order theory

iSup_mono

∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f g : ι → α}, (∀ (i : ι), f i ≤ g i) → iSup f ≤ iSup g
Defined in
Mathlib.Order.CompleteLattice.Basic
Cited by
37 results in Mathlib
Foundations
Depth 12 from the axioms · uses no axioms
Assumes
CompleteLattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.iUnion_mono · cited by 21Set.iUnion_monoiSup₂_mono · cited by 18iSup₂_monoiSup_comm · cited by 17iSup_commMeasureTheory.lintegral_iSup · cited by 16MeasureTheory.lintegral_i…biSup_mono · cited by 15biSup_monoMeasureTheory.lintegral_mono' · cited by 12MeasureTheory.lintegral_m…Set.iUnion_mono'' · cited by 9Set.iUnion_mono''iSup_sup_eq · cited by 7iSup_sup_eqiSupIndep.comp · cited by 6iSupIndep.compProbabilityTheory.Kernel.indep_iSup_directed_limsup · cited by 3Kernel.indep_iSup_directe…Monotone.iSup_nat_add · cited by 3Monotone.iSup_nat_addiSup_symmDiff_iSup_le · cited by 3iSup_symmDiff_iSup_leFormalMultilinearSeries.radius_le_smul · cited by 3FormalMultilinearSeries.r…ClosureOperator.closure_iSup_closure · cited by 2ClosureOperator.closure_i…Filter.totallyBounded_iSup · cited by 2Filter.totallyBounded_iSupiSup · cited by 2415iSupCompleteLattice · cited by 1048CompleteLatticeiSup_le · cited by 190iSup_lele_iSup_of_le · cited by 79le_iSup_of_leiSup_monoCITED BYCITES

Cites4

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

Cited by37

Results whose statement or proof uses this declaration.