Mathlib Map

Theorems · Theorem · order theory

biInf_mono

∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {p q : ι → Prop},
  (∀ (i : ι), p i → q i) → ⨅ i, ⨅ (_ : q i), f i ≤ ⨅ i, ⨅ (_ : p i), f i
Defined in
Mathlib.Order.CompleteLattice.Basic
Cited by
8 results in Mathlib
Foundations
Depth 13 from the axioms · uses no axioms
Assumes
CompleteLattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

TopologicalSpace.nhds_generateFrom · cited by 15TopologicalSpace.nhds_gen…iInf_le_iInf_of_subset · cited by 5iInf_le_iInf_of_subsetDynamics.coverMincard_monotone_time · cited by 3Dynamics.coverMincard_mon…Filter.iInf_sets_eq_finite · cited by 2Filter.iInf_sets_eq_finiteDynamics.coverMincard_antitone · cited by 2Dynamics.coverMincard_ant…iSup_iInf_ge_nat_add · cited by 2iSup_iInf_ge_nat_addDynamics.coverMincard_monotone_subset · cited by 2Dynamics.coverMincard_mon…StieltjesFunction.length_mono · cited by 1StieltjesFunction.length_…iInf · cited by 1690iInfCompleteLattice · cited by 1048CompleteLatticeiInf_mono · cited by 29iInf_monoiInf_const_mono · cited by 3iInf_const_monobiInf_monoCITED BYCITES

Cites4

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

Cited by8

Results whose statement or proof uses this declaration.