Mathlib Map

Theorems · Theorem · order theory

inf_iSup_eq

∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] (a : α) (f : ι → α), a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
Defined in
Mathlib.Order.CompleteBooleanAlgebra
Cited by
4 results in Mathlib
Foundations
Depth 18 from the axioms · uses propext, Quot.sound
Assumes
Order.Frame
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.inter_iUnion · cited by 59Set.inter_iUnioniSup_inf_iSup · cited by 3iSup_inf_iSupinf_iSup₂_eq · cited by 1inf_iSup₂_eqiSup_himp_eq · cited by 0iSup_himp_eqiSup · cited by 2415iSupinf_comm · cited by 139inf_commOrder.Frame · cited by 88Order.FrameiSup_inf_eq · cited by 7iSup_inf_eqinf_iSup_eqCITED BYCITES

Cites4

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

Cited by4

Results whose statement or proof uses this declaration.