Image

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

Statistics

Metric	Count
Definitions	0
Theorems image_lowerBounds_subset_upperBounds_image, image_upperBounds_subset_lowerBounds_image, map_bddAbove, map_bddBelow, map_isGreatest, map_isLeast, mem_lowerBounds_image, mem_upperBounds_image, image_lowerBounds_subset_upperBounds_image, image_upperBounds_subset_lowerBounds_image, map_bddAbove, map_bddBelow, map_isGreatest, map_isLeast, mem_lowerBounds_image, mem_lowerBounds_image_self, mem_upperBounds_image, mem_upperBounds_image_self, bddAbove_image2_of_bddBelow, bddBelow_image2_of_bddAbove, image2, image2_bddBelow, range_comp, range_mono, bddAbove_image2_of_bddAbove, bddBelow_image2_of_bddAbove, image2, image2_bddAbove, range_comp, range_mono, image_of_antitone, image_of_monotone, image_of_antitone, image_of_monotone, of_image, image2, isGreatest_image2_of_isLeast, isLeast_image2, isLeast_image2_of_isLeast, of_image, image2, isGreatest_image2, isGreatest_image2_of_isGreatest, isLeast_image2_of_isGreatest, image_lowerBounds_subset_lowerBounds_image, image_upperBounds_subset_upperBounds_image, map_bddAbove, map_bddBelow, map_isGreatest, map_isLeast, mem_lowerBounds_image, mem_upperBounds_image, upperBounds_image_of_directedOn_prod, image_lowerBounds_subset_lowerBounds_image, image_upperBounds_subset_upperBounds_image, map_bddAbove, map_bddBelow, map_isGreatest, map_isLeast, mem_lowerBounds_image, mem_lowerBounds_image_self, mem_upperBounds_image, mem_upperBounds_image_self, map_isGreatest, map_isLeast, mem_lowerBounds_image, mem_upperBounds_image, map_isGreatest, map_isLeast, mem_lowerBounds_image, mem_upperBounds_image, bddAbove_pi, bddAbove_prod, bddAbove_range_pi, bddAbove_range_prod, bddBelow_pi, bddBelow_prod, bddBelow_range_pi, bddBelow_range_prod, image2_lowerBounds_lowerBounds_subset, image2_lowerBounds_lowerBounds_subset_lowerBounds_image2, image2_lowerBounds_upperBounds_subset_lowerBounds_image2, image2_lowerBounds_upperBounds_subset_upperBounds_image2, image2_upperBounds_lowerBounds_subset_lowerBounds_image2, image2_upperBounds_lowerBounds_subset_upperBounds_image2, image2_upperBounds_upperBounds_subset, image2_upperBounds_upperBounds_subset_upperBounds_image2, isGLB_pi, isGLB_prod, isLUB_pi, isLUB_prod, mem_lowerBounds_image2, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds, mem_lowerBounds_image2_of_mem_upperBounds, mem_upperBounds_image2, mem_upperBounds_image2_of_mem_lowerBounds, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds	99
Total	99

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_lowerBounds_subset_upperBounds_image 📖	mathematical	Antitone	Set Set.instHasSubset Set.image lowerBounds Preorder.toLE upperBounds	—	Monotone.image_lowerBounds_subset_lowerBounds_image dual_right
image_upperBounds_subset_lowerBounds_image 📖	mathematical	Antitone	Set Set.instHasSubset Set.image upperBounds Preorder.toLE lowerBounds	—	Monotone.image_upperBounds_subset_upperBounds_image dual_right
map_bddAbove 📖	mathematical	Antitone BddAbove Preorder.toLE	BddBelow Set.image	—	Monotone.map_bddAbove dual_right
map_bddBelow 📖	mathematical	Antitone BddBelow Preorder.toLE	BddAbove Set.image	—	Monotone.map_bddBelow dual_right
map_isGreatest 📖	mathematical	Antitone IsGreatest Preorder.toLE	IsLeast Set.image	—	Monotone.map_isGreatest dual_right
map_isLeast 📖	mathematical	Antitone IsLeast Preorder.toLE	IsGreatest Set.image	—	Monotone.map_isLeast dual_right
mem_lowerBounds_image 📖	mathematical	Antitone Set Set.instMembership upperBounds Preorder.toLE	lowerBounds Set.image	—	Monotone.mem_upperBounds_image dual_right
mem_upperBounds_image 📖	mathematical	Antitone Set Set.instMembership lowerBounds Preorder.toLE	upperBounds Set.image	—	Monotone.mem_lowerBounds_image dual_right

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_lowerBounds_subset_upperBounds_image 📖	mathematical	AntitoneOn Set Set.instHasSubset	Set.image Set.instInter lowerBounds Preorder.toLE upperBounds	—	MonotoneOn.image_lowerBounds_subset_lowerBounds_image dual_right
image_upperBounds_subset_lowerBounds_image 📖	mathematical	AntitoneOn Set Set.instHasSubset	Set.image Set.instInter upperBounds Preorder.toLE lowerBounds	—	MonotoneOn.image_upperBounds_subset_upperBounds_image dual_right
map_bddAbove 📖	mathematical	AntitoneOn Set Set.instHasSubset Set.Nonempty Set.instInter upperBounds Preorder.toLE	BddBelow Set.image	—	MonotoneOn.map_bddAbove dual_right
map_bddBelow 📖	mathematical	AntitoneOn Set Set.instHasSubset Set.Nonempty Set.instInter lowerBounds Preorder.toLE	BddAbove Set.image	—	MonotoneOn.map_bddBelow dual_right
map_isGreatest 📖	mathematical	AntitoneOn IsGreatest Preorder.toLE	IsLeast Set.image	—	MonotoneOn.map_isGreatest dual_right
map_isLeast 📖	mathematical	AntitoneOn IsLeast Preorder.toLE	IsGreatest Set.image	—	MonotoneOn.map_isLeast dual_right
mem_lowerBounds_image 📖	mathematical	AntitoneOn Set Set.instHasSubset Set.instMembership upperBounds Preorder.toLE	lowerBounds Set.image	—	MonotoneOn.mem_upperBounds_image dual_right
mem_lowerBounds_image_self 📖	mathematical	AntitoneOn Set Set.instMembership upperBounds Preorder.toLE	lowerBounds Set.image	—	MonotoneOn.mem_upperBounds_image_self dual_right
mem_upperBounds_image 📖	mathematical	AntitoneOn Set Set.instHasSubset Set.instMembership lowerBounds Preorder.toLE	upperBounds Set.image	—	MonotoneOn.mem_lowerBounds_image dual_right
mem_upperBounds_image_self 📖	mathematical	AntitoneOn Set Set.instMembership lowerBounds Preorder.toLE	upperBounds Set.image	—	MonotoneOn.mem_lowerBounds_image_self dual_right

BddAbove

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove_image2_of_bddBelow 📖	mathematical	Monotone Function.swap Antitone BddAbove Preorder.toLE BddBelow	Set.image2	—	mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds
bddBelow_image2_of_bddAbove 📖	mathematical	Antitone Function.swap Monotone BddAbove Preorder.toLE BddBelow	Set.image2	—	mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds
image2 📖	mathematical	Monotone Function.swap BddAbove Preorder.toLE	Set.image2	—	mem_upperBounds_image2
image2_bddBelow 📖	mathematical	Antitone Function.swap BddAbove Preorder.toLE	BddBelow Set.image2	—	mem_lowerBounds_image2_of_mem_upperBounds
range_comp 📖	—	BddAbove Preorder.toLE Set.range Monotone	—	—	Set.range_comp Monotone.map_bddAbove
range_mono 📖	—	Preorder.toLE BddAbove Set.range	—	—	LE.le.trans Set.mem_range_self

BddBelow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove_image2_of_bddAbove 📖	mathematical	Antitone Function.swap Monotone BddBelow Preorder.toLE BddAbove	Set.image2	—	mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds
bddBelow_image2_of_bddAbove 📖	mathematical	Monotone Function.swap Antitone BddBelow Preorder.toLE BddAbove	Set.image2	—	mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds
image2 📖	mathematical	Monotone Function.swap BddBelow Preorder.toLE	Set.image2	—	mem_lowerBounds_image2
image2_bddAbove 📖	mathematical	Antitone Function.swap BddBelow Preorder.toLE	BddAbove Set.image2	—	mem_upperBounds_image2_of_mem_lowerBounds
range_comp 📖	—	BddBelow Preorder.toLE Set.range Monotone	—	—	Set.range_comp Monotone.map_bddBelow
range_mono 📖	—	Preorder.toLE BddBelow Set.range	—	—	BddAbove.range_mono

IsCofinalFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_of_antitone 📖	mathematical	IsCofinalFor Preorder.toLE Antitone	IsCoinitialFor Set.image	—	—
image_of_monotone 📖	mathematical	IsCofinalFor Preorder.toLE Monotone	Set.image	—	—

IsCoinitialFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_of_antitone 📖	mathematical	IsCoinitialFor Preorder.toLE Antitone	IsCofinalFor Set.image	—	—
image_of_monotone 📖	mathematical	IsCoinitialFor Preorder.toLE Monotone	Set.image	—	—

IsGLB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_image 📖	—	Preorder.toLE IsGLB Set.image	—	—	Set.mem_image_of_mem Monotone.mem_lowerBounds_image

IsGreatest

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image2 📖	mathematical	Monotone Function.swap IsGreatest Preorder.toLE	Set.image2	—	Set.mem_image2_of_mem mem_upperBounds_image2
isGreatest_image2_of_isLeast 📖	mathematical	Monotone Function.swap Antitone IsGreatest Preorder.toLE IsLeast	Set.image2	—	Set.mem_image2_of_mem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds
isLeast_image2 📖	mathematical	Antitone Function.swap IsGreatest Preorder.toLE	IsLeast Set.image2	—	Set.mem_image2_of_mem mem_lowerBounds_image2_of_mem_upperBounds
isLeast_image2_of_isLeast 📖	mathematical	Antitone Function.swap Monotone IsGreatest Preorder.toLE IsLeast	Set.image2	—	Set.mem_image2_of_mem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds

IsLUB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_image 📖	—	Preorder.toLE IsLUB Set.image	—	—	Set.mem_image_of_mem Monotone.mem_upperBounds_image

IsLeast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image2 📖	mathematical	Monotone Function.swap IsLeast Preorder.toLE	Set.image2	—	Set.mem_image2_of_mem mem_lowerBounds_image2
isGreatest_image2 📖	mathematical	Antitone Function.swap IsLeast Preorder.toLE	IsGreatest Set.image2	—	Set.mem_image2_of_mem mem_upperBounds_image2_of_mem_lowerBounds
isGreatest_image2_of_isGreatest 📖	mathematical	Antitone Function.swap Monotone IsLeast Preorder.toLE IsGreatest	Set.image2	—	Set.mem_image2_of_mem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds
isLeast_image2_of_isGreatest 📖	mathematical	Monotone Function.swap Antitone IsLeast Preorder.toLE IsGreatest	Set.image2	—	Set.mem_image2_of_mem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_lowerBounds_subset_lowerBounds_image 📖	mathematical	Monotone	Set Set.instHasSubset Set.image lowerBounds Preorder.toLE	—	image_upperBounds_subset_upperBounds_image dual
image_upperBounds_subset_upperBounds_image 📖	mathematical	Monotone	Set Set.instHasSubset Set.image upperBounds Preorder.toLE	—	mem_upperBounds_image
map_bddAbove 📖	mathematical	Monotone BddAbove Preorder.toLE	Set.image	—	mem_upperBounds_image
map_bddBelow 📖	mathematical	Monotone BddBelow Preorder.toLE	Set.image	—	mem_lowerBounds_image
map_isGreatest 📖	mathematical	Monotone IsGreatest Preorder.toLE	Set.image	—	Set.mem_image_of_mem mem_upperBounds_image
map_isLeast 📖	mathematical	Monotone IsLeast Preorder.toLE	Set.image	—	Set.mem_image_of_mem mem_lowerBounds_image
mem_lowerBounds_image 📖	mathematical	Monotone Set Set.instMembership lowerBounds Preorder.toLE	Set.image	—	Set.forall_mem_image
mem_upperBounds_image 📖	mathematical	Monotone Set Set.instMembership upperBounds Preorder.toLE	Set.image	—	Set.forall_mem_image
upperBounds_image_of_directedOn_prod 📖	mathematical	Monotone Prod.instPreorder DirectedOn Prod.instLE_mathlib Preorder.toLE	upperBounds Set.image SProd.sprod Set Set.instSProd	—	le_antisymm upperBounds_mono_of_isCofinalFor IsCofinalFor.image_of_monotone DirectedOn.isCofinalFor_fst_image_prod_snd_image upperBounds_mono_set Set.image_mono Set.subset_fst_image_prod_snd_image

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_lowerBounds_subset_lowerBounds_image 📖	mathematical	MonotoneOn Set Set.instHasSubset	Set.image Set.instInter lowerBounds Preorder.toLE	—	image_upperBounds_subset_upperBounds_image dual
image_upperBounds_subset_upperBounds_image 📖	mathematical	MonotoneOn Set Set.instHasSubset	Set.image Set.instInter upperBounds Preorder.toLE	—	mem_upperBounds_image
map_bddAbove 📖	mathematical	MonotoneOn Set Set.instHasSubset Set.Nonempty Set.instInter upperBounds Preorder.toLE	BddAbove Set.image	—	mem_upperBounds_image
map_bddBelow 📖	mathematical	MonotoneOn Set Set.instHasSubset Set.Nonempty Set.instInter lowerBounds Preorder.toLE	BddBelow Set.image	—	mem_lowerBounds_image
map_isGreatest 📖	mathematical	MonotoneOn IsGreatest Preorder.toLE	Set.image	—	Set.mem_image_of_mem mem_upperBounds_image_self
map_isLeast 📖	mathematical	MonotoneOn IsLeast Preorder.toLE	Set.image	—	Set.mem_image_of_mem mem_lowerBounds_image_self
mem_lowerBounds_image 📖	mathematical	MonotoneOn Set Set.instHasSubset Set.instMembership lowerBounds Preorder.toLE	Set.image	—	Set.forall_mem_image
mem_lowerBounds_image_self 📖	mathematical	MonotoneOn Set Set.instMembership lowerBounds Preorder.toLE	Set.image	—	mem_lowerBounds_image subset_rfl Set.instReflSubset
mem_upperBounds_image 📖	mathematical	MonotoneOn Set Set.instHasSubset Set.instMembership upperBounds Preorder.toLE	Set.image	—	Set.forall_mem_image
mem_upperBounds_image_self 📖	mathematical	MonotoneOn Set Set.instMembership upperBounds Preorder.toLE	Set.image	—	mem_upperBounds_image subset_rfl Set.instReflSubset

StrictAnti

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_isGreatest 📖	mathematical	StrictAnti PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsGreatest Preorder.toLE Set.image IsLeast	—	injective mem_upperBounds_image
map_isLeast 📖	mathematical	StrictAnti PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsLeast Preorder.toLE Set.image IsGreatest	—	injective mem_lowerBounds_image
mem_lowerBounds_image 📖	mathematical	StrictAnti PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership lowerBounds Preorder.toLE Set.image upperBounds	—	le_iff_ge
mem_upperBounds_image 📖	mathematical	StrictAnti PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership upperBounds Preorder.toLE Set.image lowerBounds	—	le_iff_ge

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_isGreatest 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsGreatest Preorder.toLE Set.image	—	injective mem_upperBounds_image
map_isLeast 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsLeast Preorder.toLE Set.image	—	injective mem_lowerBounds_image
mem_lowerBounds_image 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership lowerBounds Preorder.toLE Set.image	—	le_iff_le
mem_upperBounds_image 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership upperBounds Preorder.toLE Set.image	—	le_iff_le

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove_pi 📖	mathematical	—	BddAbove Pi.hasLe Preorder.toLE Set.image Function.eval	—	Set.forall_mem_image Set.Nonempty.some_mem Set.mem_image_of_mem
bddAbove_prod 📖	mathematical	—	BddAbove Prod.instLE_mathlib Preorder.toLE Set.image	—	Set.forall_mem_image Set.mem_image_of_mem
bddAbove_range_pi 📖	mathematical	—	BddAbove Pi.hasLe Preorder.toLE Set.range	—	—
bddAbove_range_prod 📖	mathematical	—	BddAbove Prod.instLE_mathlib Preorder.toLE Set.range	—	—
bddBelow_pi 📖	mathematical	—	BddBelow Pi.hasLe Preorder.toLE Set.image Function.eval	—	bddAbove_pi
bddBelow_prod 📖	mathematical	—	BddBelow Prod.instLE_mathlib Preorder.toLE Set.image	—	bddAbove_prod
bddBelow_range_pi 📖	mathematical	—	BddBelow Pi.hasLe Preorder.toLE Set.range	—	bddAbove_range_pi
bddBelow_range_prod 📖	mathematical	—	BddBelow Prod.instLE_mathlib Preorder.toLE Set.range	—	bddAbove_range_prod
image2_lowerBounds_lowerBounds_subset 📖	mathematical	Monotone Function.swap	Set Set.instHasSubset Set.image2 lowerBounds Preorder.toLE	—	Set.image2_subset_iff mem_lowerBounds_image2
image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 📖	mathematical	Antitone Function.swap	Set Set.instHasSubset Set.image2 upperBounds Preorder.toLE lowerBounds	—	Set.image2_subset_iff mem_lowerBounds_image2_of_mem_upperBounds
image2_lowerBounds_upperBounds_subset_lowerBounds_image2 📖	mathematical	Monotone Function.swap Antitone	Set Set.instHasSubset Set.image2 lowerBounds Preorder.toLE upperBounds	—	Set.image2_subset_iff mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds
image2_lowerBounds_upperBounds_subset_upperBounds_image2 📖	mathematical	Antitone Function.swap Monotone	Set Set.instHasSubset Set.image2 lowerBounds Preorder.toLE upperBounds	—	Set.image2_subset_iff mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds
image2_upperBounds_lowerBounds_subset_lowerBounds_image2 📖	mathematical	Antitone Function.swap Monotone	Set Set.instHasSubset Set.image2 upperBounds Preorder.toLE lowerBounds	—	Set.image2_subset_iff mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds
image2_upperBounds_lowerBounds_subset_upperBounds_image2 📖	mathematical	Monotone Function.swap Antitone	Set Set.instHasSubset Set.image2 upperBounds Preorder.toLE lowerBounds	—	Set.image2_subset_iff mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds
image2_upperBounds_upperBounds_subset 📖	mathematical	Monotone Function.swap	Set Set.instHasSubset Set.image2 upperBounds Preorder.toLE	—	Set.image2_subset_iff mem_upperBounds_image2
image2_upperBounds_upperBounds_subset_upperBounds_image2 📖	mathematical	Antitone Function.swap	Set Set.instHasSubset Set.image2 lowerBounds Preorder.toLE upperBounds	—	Set.image2_subset_iff mem_upperBounds_image2_of_mem_lowerBounds
isGLB_pi 📖	mathematical	—	IsGLB Pi.hasLe Preorder.toLE Set.image Function.eval	—	isLUB_pi
isGLB_prod 📖	mathematical	—	IsGLB Prod.instLE_mathlib Preorder.toLE Set.image	—	isLUB_prod
isLUB_pi 📖	mathematical	—	IsLUB Pi.hasLe Preorder.toLE Set.image Function.eval	—	Monotone.mem_upperBounds_image Function.monotone_eval le_update_iff Set.mem_image_of_mem Function.update_self
isLUB_prod 📖	mathematical	—	IsLUB Prod.instLE_mathlib Preorder.toLE Set.image	—	Monotone.mem_upperBounds_image monotone_fst Set.mem_image_of_mem monotone_snd
mem_lowerBounds_image2 📖	mathematical	Monotone Function.swap Set Set.instMembership lowerBounds Preorder.toLE	Set.image2	—	Set.forall_mem_image2 LE.le.trans
mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds 📖	mathematical	Antitone Function.swap Monotone Set Set.instMembership upperBounds Preorder.toLE lowerBounds	Set.image2	—	Set.forall_mem_image2 LE.le.trans
mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds 📖	mathematical	Monotone Function.swap Antitone Set Set.instMembership lowerBounds Preorder.toLE upperBounds	Set.image2	—	Set.forall_mem_image2 LE.le.trans
mem_lowerBounds_image2_of_mem_upperBounds 📖	mathematical	Antitone Function.swap Set Set.instMembership upperBounds Preorder.toLE	lowerBounds Set.image2	—	Set.forall_mem_image2 LE.le.trans
mem_upperBounds_image2 📖	mathematical	Monotone Function.swap Set Set.instMembership upperBounds Preorder.toLE	Set.image2	—	Set.forall_mem_image2 LE.le.trans
mem_upperBounds_image2_of_mem_lowerBounds 📖	mathematical	Antitone Function.swap Set Set.instMembership lowerBounds Preorder.toLE	upperBounds Set.image2	—	Set.forall_mem_image2 LE.le.trans
mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds 📖	mathematical	Monotone Function.swap Antitone Set Set.instMembership upperBounds Preorder.toLE lowerBounds	Set.image2	—	Set.forall_mem_image2 LE.le.trans
mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds 📖	mathematical	Antitone Function.swap Monotone Set Set.instMembership lowerBounds Preorder.toLE upperBounds	Set.image2	—	Set.forall_mem_image2 LE.le.trans

---

← Back to Index