Theorems · Theorem · order theory
Set.Icc_toDual
∀ {α : Type u_1} [inst : Preorder α] {a b : α},
Set.Icc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Icc b a- Defined in
- Mathlib.Order.Interval.Set.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement · cited by 53,352
- Equivstatement · cited by 8,337
- Preorderstatement and proof · cited by 7,952
- Set.preimagestatement · cited by 4,946
- Set.extproof · cited by 2,266
- Set.Iccstatement · cited by 1,702
- OrderDualstatement and proof · cited by 927
- OrderDual.toDualstatement · cited by 481
- OrderDual.ofDualstatement · cited by 400
Cited by13
Results whose statement or proof uses this declaration.
- LocallyBoundedVariationOn.ofDualproof · cited by 2
- TFAE_mem_nhdsLEproof · cited by 2
- BoundedVariationOn.tendsto_eVariationOn_Icc_zero_rightproof · cited by 1
- Set.uIcc_toDualproof · cited by 1
- mem_nhdsLE_iff_exists_Icc_subsetproof · cited by 1
- IsClosed.mem_of_ge_of_forall_exists_ltproof · cited by 1
- NonemptyInterval.coe_dualproof · cited by 1
- LocallyBoundedVariationOn.tendsto_eVariationOn_Icc_rightproof · cited by 1
- BoundedVariationOn.tendsto_eVariationOn_Icc_rightproof · cited by 0
- AntitoneOn.sInf_image_Iccproof · cited by 0
- AntitoneOn.sSup_image_Iccproof · cited by 0
- eVariationOn.eVariationOn_Ico_eq_Icc_of_continuousWithinAtproof · cited by 0