OrderIso

📁 Source: Mathlib/Order/Bounds/OrderIso.lean

Statistics

Metric	Count
Definitions	0
Theorems isGLB_image, isGLB_image', isGLB_preimage, isGLB_preimage', isLUB_image, isLUB_image', isLUB_preimage, isLUB_preimage', lowerBounds_image, upperBounds_image	10
Total	10

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGLB_image 📖	mathematical	—	IsGLB Preorder.toLE Set.image DFunLike.coe OrderIso instFunLikeOrderIso symm	—	isLUB_image
isGLB_image' 📖	mathematical	—	IsGLB Preorder.toLE Set.image DFunLike.coe OrderIso instFunLikeOrderIso	—	isLUB_image'
isGLB_preimage 📖	mathematical	—	IsGLB Preorder.toLE Set.preimage DFunLike.coe OrderIso instFunLikeOrderIso	—	isLUB_preimage
isGLB_preimage' 📖	mathematical	—	IsGLB Preorder.toLE Set.preimage DFunLike.coe OrderIso instFunLikeOrderIso symm	—	isLUB_preimage'
isLUB_image 📖	mathematical	—	IsLUB Preorder.toLE Set.image DFunLike.coe OrderIso instFunLikeOrderIso symm	—	IsLUB.of_image instOrderIsoClass apply_symm_apply symm_image_image
isLUB_image' 📖	mathematical	—	IsLUB Preorder.toLE Set.image DFunLike.coe OrderIso instFunLikeOrderIso	—	isLUB_image symm_apply_apply
isLUB_preimage 📖	mathematical	—	IsLUB Preorder.toLE Set.preimage DFunLike.coe OrderIso instFunLikeOrderIso	—	symm_symm image_eq_preimage_symm isLUB_image
isLUB_preimage' 📖	mathematical	—	IsLUB Preorder.toLE Set.preimage DFunLike.coe OrderIso instFunLikeOrderIso symm	—	isLUB_preimage apply_symm_apply
lowerBounds_image 📖	mathematical	—	lowerBounds Preorder.toLE Set.image DFunLike.coe OrderIso instFunLikeOrderIso	—	upperBounds_image
upperBounds_image 📖	mathematical	—	upperBounds Preorder.toLE Set.image DFunLike.coe OrderIso instFunLikeOrderIso	—	Set.Subset.antisymm le_symm_apply Set.mem_image_of_mem apply_symm_apply Monotone.image_upperBounds_subset_upperBounds_image monotone

---

← Back to Index