Theorems · Theorem · order theory
OrderIso.map_sInf_eq_sInf_symm_preimage
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α),
f (sInf s) = sInf (⇑f.symm ⁻¹' s)- Defined in
- Mathlib.Order.CompleteLattice.Basic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Quot.sound
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 and proof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Set.preimagestatement and proof · cited by 4,946
- CompleteLatticestatement and proof · cited by 1,048
- InfSet.sInfstatement and proof · cited by 935
- OrderIsostatement and proof · cited by 874
- OrderIso.symmstatement and proof · cited by 475
- sInf_imageproof · cited by 25
- OrderIso.image_eq_preimage_symmproof · cited by 13
- OrderIso.map_sInfproof · cited by 3
Cited by18
Results whose statement or proof uses this declaration.
- AddSubmonoid.op_sInfproof · cited by 1
- Subring.op_sInfproof · cited by 1
- Subsemigroup.op_sInfproof · cited by 1
- Submonoid.op_sInfproof · cited by 1
- Subgroup.op_sInfproof · cited by 1
- Subsemiring.op_sInfproof · cited by 1
- AddSubsemigroup.op_sInfproof · cited by 1
- AddSubgroup.op_sInfproof · cited by 1
- Subsemigroup.unop_sInfproof · cited by 0
- Subgroup.unop_sInfproof · cited by 0
- AddSubgroup.unop_sInfproof · cited by 0
- Subsemiring.unop_sInfproof · cited by 0