Theorems · Theorem · order theory
iInf_image
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_8} {f : β → γ} {g : γ → α} {t : Set β},
⨅ c ∈ f '' t, g c = ⨅ b ∈ t, g (f b)- Defined in
- Mathlib.Order.CompleteLattice.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
- Assumes
- CompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.imagestatement and proof · cited by 5,609
- iInfstatement and proof · cited by 1,690
- CompleteLatticestatement and proof · cited by 1,048
- InfSet.sInfproof · cited by 935
- Set.image_compproof · cited by 142
- sInf_imageproof · cited by 25
Cited by14
Results whose statement or proof uses this declaration.
- Metric.infEDist_imageproof · cited by 7
- IsLocalization.height_underproof · cited by 6
- ContinuousMap.nhds_compactOpenproof · cited by 4
- Ideal.comap_sInf'proof · cited by 3
- Set.BijOn.iInf_compproof · cited by 2
- Function.coframeMinimalAxiomsproof · cited by 2
- MeasureTheory.Measure.inf_applyproof · cited by 2
- MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrictproof · cited by 1
- iInf_image2proof · cited by 1
- Finset.iInf_finset_imageproof · cited by 1
- MeasureTheory.Measure.sInf_caratheodoryproof · cited by 1
- Filter.smallSets_eq_generateproof · cited by 1