Max

📁 Source: Mathlib/Data/Finset/Max.lean

Statistics

Metric	Count
Definitions max, max', min, min'	4
Theorems card_le_diff_of_interleaved, card_le_of_interleaved, coe_max', coe_min', exists_max_image, exists_min_image, exists_next_left, exists_next_right, induction_on_max, induction_on_max_value, induction_on_min, induction_on_min_value, isGLB_iff_isLeast, isGLB_mem, isGreatest_max', isLUB_iff_isGreatest, isLUB_mem, isLeast_min', le_max, le_max', le_max_of_eq, le_min, le_min', le_min'_iff, le_min_iff, lt_max'_of_mem_erase_max', lt_min'_iff, map_ofDual_max, map_ofDual_min, map_toDual_max, map_toDual_min, max'_eq_iff, max'_eq_sup', max'_erase_ne_self, max'_image, max'_insert, max'_le, max'_le_iff, max'_lt_iff, max'_mem, max'_pair, max'_singleton, max'_subset, max'_union, max_empty, max_eq_bot, max_eq_sup_coe, max_eq_sup_withBot, max_eq_top, max_erase_ne_self, max_insert, max_le, max_le_iff, max_mem_image_coe, max_mem_insert_bot_image_coe, max_mono, max_of_mem, max_of_nonempty, max_pair, max_singleton, max_union, mem_of_max, mem_of_min, min'_eq_iff, min'_eq_inf', min'_erase_ne_self, min'_image, min'_insert, min'_le, min'_le_max', min'_lt_max', min'_lt_max'_of_card, min'_lt_of_mem_erase_min', min'_mem, min'_pair, min'_singleton, min'_subset, min'_union, min_empty, min_eq_bot, min_eq_inf_withTop, min_eq_top, min_erase_ne_self, min_insert, min_le, min_le_of_eq, min_mem_image_coe, min_mem_insert_top_image_coe, min_mono, min_of_mem, min_of_nonempty, min_pair, min_singleton, min_union, notMem_of_coe_lt_min, notMem_of_lt_min, notMem_of_max_lt, notMem_of_max_lt_coe, ofDual_max', ofDual_min', toDual_max', toDual_min', map_finset_max', map_finset_min', exists_max_image, exists_min_image	106
Total	110

Finset

Definitions

Name	Category	Theorems
max 📖	CompOp	24 math math: max_union, map_ofDual_max, max_singleton, max_mono, max_pair, max_eq_sup_coe, map_toDual_max, max_mem_image_coe, max_mem_insert_bot_image_coe, map_toDual_min, max_le_iff, max_eq_sup_withBot, max_zero, max_eq_bot, max_eq_top, max_empty, max_insert, max_of_nonempty, map_ofDual_min, coe_max', max_le, le_max, max_one, max_of_mem
max' 📖	CompOp	39 math math: sorted_last_eq_max'_aux, max'_singleton, max'_le, max'_one, ciSup_eq_max'_image, Colex.toColex_lt_toColex_iff_max'_mem, Colex.le_iff_max'_mem, max'_le_iff, max'_mem, Colex.toColex_le_toColex_iff_max'_mem, toDual_min', sorted_last_eq_max', AddMonoid.exponent_eq_max'_addOrderOf, max'_subset, max'_pair, max'_zero, isGreatest_max', Polynomial.natDegree_eq_support_max', max'_image, max'_eq_sup', orderEmbOfFin_last, max'_insert, max'_eq_sorted_last, toDual_max', Nonempty.csSup_eq_max', min'_lt_max', max'_union, min'_lt_max'_of_card, min'_le_max', Monoid.exponent_eq_max'_orderOf, max'_eq_iff, ofDual_min', le_max', Colex.lt_iff_max'_mem, Monotone.map_finset_max', Nonempty.ciSup_eq_max'_image, coe_max', max'_lt_iff, ofDual_max'
min 📖	CompOp	23 math math: min_zero, min_eq_inf_withTop, min_of_mem, map_ofDual_max, min_union, min_le, min_one, map_toDual_max, le_min, min_empty, map_toDual_min, min_mem_image_coe, coe_min', min_eq_top, min_eq_bot, min_pair, min_of_nonempty, le_min_iff, min_singleton, min_insert, min_mono, map_ofDual_min, min_mem_insert_top_image_coe
min' 📖	CompOp	36 math math: min'_union, MulArchimedeanClass.mk_prod, min'_le, sorted_zero_eq_min'_aux, toDual_min', min'_mem, orderEmbOfFin_zero, sorted_zero_eq_min', Monotone.map_finset_min', Nonempty.csInf_eq_min', coe_min', min'_subset, min'_zero, toDual_max', ciInf_eq_min'_image, min'_lt_max', min'_lt_max'_of_card, Colex.shadow_initSeg, min'_insert, min'_eq_sorted_zero, min'_le_max', Polynomial.natTrailingDegree_eq_support_min', min'_singleton, ofDual_min', min'_image, min'_pair, Colex.erase_le_erase_min', min'_eq_iff, min'_one, le_min'_iff, lt_min'_iff, le_min', ArchimedeanClass.mk_sum, ofDual_max', min'_eq_inf', isLeast_min'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_le_diff_of_interleaved 📖	mathematical	Finset instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	card instSDiff LinearOrder.toDecidableEq	—	card_le_of_interleaved mem_sdiff
card_le_of_interleaved 📖	mathematical	Finset instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	card	—	exists_next_right LT.lt.not_ge LT.lt.trans_le min_le mem_filter lt_inf_iff WithTop.coe_lt_top WithTop.coe_lt_coe LT.lt.trans card_image_of_injOn StrictMonoOn.injOn card_mono image_subset_iff insert_subset_insert image_subset_image filter_subset min_mem_insert_top_image_coe LE.le.trans card_insert_le card_image_le
coe_max' 📖	mathematical	Nonempty	WithBot.some max' max	—	coe_sup'
coe_min' 📖	mathematical	Nonempty	WithTop.some min' min	—	coe_inf'
exists_max_image 📖	mathematical	Nonempty	Finset instMembership Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	max_of_nonempty Nonempty.image mem_image mem_of_max le_max_of_eq mem_image_of_mem
exists_min_image 📖	mathematical	Nonempty	Finset instMembership Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_max_image
exists_next_left 📖	mathematical	Finset instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE	—	exists_next_right
exists_next_right 📖	mathematical	Finset instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE	—	mem_filter min'_mem min'_le
induction_on_max 📖	—	Finset instEmptyCollection instInsert	—	—	eraseInduction eq_empty_or_nonempty max'_mem insert_erase lt_max'_of_mem_erase_max'
induction_on_max_value 📖	—	Finset instEmptyCollection instInsert	—	—	eraseInduction eq_empty_or_nonempty max'_mem insert_erase notMem_erase le_max' mem_image_of_mem mem_of_mem_erase
induction_on_min 📖	—	Finset instEmptyCollection instInsert	—	—	induction_on_max
induction_on_min_value 📖	—	Finset instEmptyCollection instInsert	—	—	induction_on_max_value
isGLB_iff_isLeast 📖	mathematical	Nonempty	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset instSetLike IsLeast	—	le_antisymm mem_upperBounds mem_lowerBounds IsGreatest.eq_1 IsGLB.eq_1 min'_mem min'_le isLeast_min' IsLeast.isGLB
isGLB_mem 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset instSetLike Nonempty	instMembership	—	mem_coe isGLB_iff_isLeast
isGreatest_max' 📖	mathematical	Nonempty	IsGreatest Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset instSetLike max'	—	max'_mem le_max'
isLUB_iff_isGreatest 📖	mathematical	Nonempty	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset instSetLike IsGreatest	—	isGLB_iff_isLeast
isLUB_mem 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset instSetLike Nonempty	instMembership	—	isGLB_mem
isLeast_min' 📖	mathematical	Nonempty	IsLeast Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset instSetLike min'	—	min'_mem min'_le
le_max 📖	mathematical	Finset instMembership	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.some max	—	le_sup
le_max' 📖	mathematical	Finset instMembership	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder max'	—	le_max_of_eq WithBot.coe_unbot
le_max_of_eq 📖	mathematical	Finset instMembership max WithBot.some	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	WithBot.coe_le_coe LE.le.trans le_max Eq.le
le_min 📖	mathematical	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.some	min	—	le_inf
le_min' 📖	mathematical	Nonempty Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	min'	—	min'_mem
le_min'_iff 📖	mathematical	Nonempty	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min'	—	le_isGLB_iff IsLeast.isGLB isLeast_min'
le_min_iff 📖	mathematical	—	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min WithTop.some	—	le_inf_iff
lt_max'_of_mem_erase_max' 📖	mathematical	Nonempty Finset instMembership erase max'	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	lt_of_le_of_ne le_max' mem_of_mem_erase notMem_erase
lt_min'_iff 📖	mathematical	Nonempty	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min'	—	max'_lt_iff
map_ofDual_max 📖	mathematical	—	WithBot.map OrderDual DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual max OrderDual.instLinearOrder min image LinearOrder.toDecidableEq	—	min_eq_inf_withTop inf_image WithTop.map_id
map_ofDual_min 📖	mathematical	—	WithTop.map OrderDual DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual min OrderDual.instLinearOrder max image LinearOrder.toDecidableEq	—	max_eq_sup_withBot sup_image WithBot.map_id
map_toDual_max 📖	mathematical	—	WithBot.map OrderDual DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual max min OrderDual.instLinearOrder image OrderDual.instDecidableEq LinearOrder.toDecidableEq	—	min_eq_inf_withTop inf_image WithTop.map_id
map_toDual_min 📖	mathematical	—	WithTop.map OrderDual DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual min max OrderDual.instLinearOrder image OrderDual.instDecidableEq LinearOrder.toDecidableEq	—	max_eq_sup_withBot sup_image WithBot.map_id
max'_eq_iff 📖	mathematical	Nonempty	max' Finset instMembership Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	max'_mem le_max' le_antisymm max'_le
max'_eq_sup' 📖	mathematical	Nonempty	max' sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—
max'_erase_ne_self 📖	—	Nonempty erase LinearOrder.toDecidableEq	—	—	ne_of_mem_erase max'_mem
max'_image 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nonempty image LinearOrder.toDecidableEq	max' Nonempty.of_image	—	Nonempty.of_image sup'_image comp_sup'_eq_sup'_comp Monotone.map_max
max'_insert 📖	mathematical	Nonempty	max' Finset instInsert LinearOrder.toDecidableEq insert_nonempty SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	IsGreatest.unique insert_nonempty isGreatest_max' coe_insert IsGreatest.insert
max'_le 📖	mathematical	Nonempty Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	max'	—	max'_mem
max'_le_iff 📖	mathematical	Nonempty	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder max'	—	isLUB_le_iff IsGreatest.isLUB isGreatest_max'
max'_lt_iff 📖	mathematical	Nonempty	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder max'	—	LE.le.trans_lt le_max' max'_mem
max'_mem 📖	mathematical	Nonempty	Finset instMembership max'	—	mem_of_max sup'_congr coe_sup'
max'_pair 📖	mathematical	—	max' Finset instInsert LinearOrder.toDecidableEq instSingleton insert_nonempty SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	insert_nonempty max'_insert max'_singleton
max'_singleton 📖	mathematical	—	max' Finset instSingleton singleton_nonempty	—	singleton_nonempty sup'_congr
max'_subset 📖	mathematical	Nonempty Finset instHasSubset	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder max' Nonempty.mono	—	le_max' max'_mem
max'_union 📖	mathematical	Nonempty	max' Finset instUnion LinearOrder.toDecidableEq Nonempty.mono subset_union_left SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	sup'_union
max_empty 📖	mathematical	—	max Finset instEmptyCollection Bot.bot WithBot WithBot.bot	—	—
max_eq_bot 📖	mathematical	—	max Bot.bot WithBot WithBot.bot Finset instEmptyCollection	—	eq_empty_or_nonempty max_of_nonempty max_empty
max_eq_sup_coe 📖	mathematical	—	max sup WithBot WithBot.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.instOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder WithBot.some	—	—
max_eq_sup_withBot 📖	mathematical	—	max sup WithBot WithBot.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.instOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder WithBot.some	—	—
max_eq_top 📖	mathematical	—	max Top.top WithBot WithBot.instTop OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset instMembership	—	sup_eq_top_iff WithBot.nontrivial top_nonempty
max_erase_ne_self 📖	—	—	—	—	ne_of_eq_of_ne coe_max' Iff.not WithBot.coe_eq_coe max'_erase_ne_self max_empty WithBot.bot_ne_coe
max_insert 📖	mathematical	—	max Finset instInsert LinearOrder.toDecidableEq WithBot SemilatticeSup.toMax WithBot.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.some	—	fold_insert_idem instCommutativeMax instAssociativeMax max_idem
max_le 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.some	max	—	sup_le
max_le_iff 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder max WithBot.some	—	sup_le_iff
max_mem_image_coe 📖	mathematical	Nonempty	WithBot Finset instMembership image WithBot.decidableEq LinearOrder.toDecidableEq WithBot.some max	—	mem_image max'_mem coe_max'
max_mem_insert_bot_image_coe 📖	mathematical	—	WithBot Finset instMembership instInsert WithBot.decidableEq LinearOrder.toDecidableEq Bot.bot WithBot.bot image WithBot.some max	—	mem_insert max_eq_bot max_mem_image_coe eq_empty_or_nonempty
max_mono 📖	mathematical	Finset instHasSubset	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder max	—	sup_mono
max_of_mem 📖	mathematical	Finset instMembership	max WithBot.some	—	WithBot.le_iff_forall le_sup
max_of_nonempty 📖	mathematical	Nonempty	max WithBot.some	—	max_of_mem
max_pair 📖	mathematical	—	max Finset instInsert LinearOrder.toDecidableEq instSingleton WithBot SemilatticeSup.toMax WithBot.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.some	—	max_insert max_singleton
max_singleton 📖	mathematical	—	max Finset instSingleton WithBot.some	—	instLawfulSingleton max_insert
max_union 📖	mathematical	—	max Finset instUnion LinearOrder.toDecidableEq WithBot SemilatticeSup.toMax WithBot.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	sup_union
mem_of_max 📖	mathematical	max WithBot.some	Finset instMembership	—	induction_on
mem_of_min 📖	mathematical	min WithTop.some	Finset instMembership	—	mem_of_max
min'_eq_iff 📖	mathematical	Nonempty	min' Finset instMembership Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	min'_mem min'_le le_antisymm le_min'
min'_eq_inf' 📖	mathematical	Nonempty	min' inf' Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—
min'_erase_ne_self 📖	—	Nonempty erase LinearOrder.toDecidableEq	—	—	ne_of_mem_erase min'_mem
min'_image 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nonempty image LinearOrder.toDecidableEq	min' Nonempty.of_image	—	Nonempty.of_image inf'_image comp_inf'_eq_inf'_comp Monotone.map_min
min'_insert 📖	mathematical	Nonempty	min' Finset instInsert LinearOrder.toDecidableEq insert_nonempty SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	IsLeast.unique insert_nonempty isLeast_min' coe_insert IsLeast.insert
min'_le 📖	mathematical	Finset instMembership	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min'	—	min_le_of_eq WithTop.coe_untop
min'_le_max' 📖	mathematical	Nonempty	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min' max'	—	min'_le max'_mem
min'_lt_max' 📖	mathematical	Finset instMembership	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min' max'	—	isGLB_lt_isLUB_of_ne IsLeast.isGLB isLeast_min' IsGreatest.isLUB isGreatest_max'
min'_lt_max'_of_card 📖	mathematical	card	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min' Nonempty card_pos max'	—	card_pos one_lt_card min'_lt_max'
min'_lt_of_mem_erase_min' 📖	mathematical	Nonempty Finset instMembership erase min'	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	lt_max'_of_mem_erase_max'
min'_mem 📖	mathematical	Nonempty	Finset instMembership min'	—	mem_of_min inf'_congr coe_inf'
min'_pair 📖	mathematical	—	min' Finset instInsert LinearOrder.toDecidableEq instSingleton insert_nonempty SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	insert_nonempty min'_insert min'_singleton
min'_singleton 📖	mathematical	—	min' Finset instSingleton singleton_nonempty	—	singleton_nonempty inf'_congr
min'_subset 📖	mathematical	Nonempty Finset instHasSubset	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min' Nonempty.mono	—	min'_le min'_mem
min'_union 📖	mathematical	Nonempty	min' Finset instUnion LinearOrder.toDecidableEq Nonempty.mono subset_union_left SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	inf'_union
min_empty 📖	mathematical	—	min Finset instEmptyCollection Top.top WithTop WithTop.top	—	—
min_eq_bot 📖	mathematical	—	min Bot.bot WithTop WithTop.instBot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset instMembership	—	max_eq_top
min_eq_inf_withTop 📖	mathematical	—	min inf WithTop WithTop.semilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.instOrderTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder WithTop.some	—	—
min_eq_top 📖	mathematical	—	min Top.top WithTop WithTop.top Finset instEmptyCollection	—	—
min_erase_ne_self 📖	—	—	—	—	map_toDual_min image_erase Equiv.injective WithTop.map_coe max_erase_ne_self
min_insert 📖	mathematical	—	min Finset instInsert LinearOrder.toDecidableEq WithTop SemilatticeInf.toMin WithTop.semilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.some	—	fold_insert_idem instCommutativeMin instAssociativeMin min_idem
min_le 📖	mathematical	Finset instMembership	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min WithTop.some	—	inf_le
min_le_of_eq 📖	mathematical	Finset instMembership min WithTop.some	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	WithTop.coe_le_coe LE.le.trans Eq.ge min_le
min_mem_image_coe 📖	mathematical	Nonempty	WithTop Finset instMembership image WithTop.decidableEq LinearOrder.toDecidableEq WithTop.some min	—	mem_image min'_mem coe_min'
min_mem_insert_top_image_coe 📖	mathematical	—	WithTop Finset instMembership instInsert WithTop.decidableEq LinearOrder.toDecidableEq Top.top WithTop.top image WithTop.some min	—	mem_insert min_eq_top min_mem_image_coe eq_empty_or_nonempty
min_mono 📖	mathematical	Finset instHasSubset	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min	—	inf_mono
min_of_mem 📖	mathematical	Finset instMembership	min WithTop.some	—	WithTop.le_iff_forall inf_le
min_of_nonempty 📖	mathematical	Nonempty	min WithTop.some	—	min_of_mem
min_pair 📖	mathematical	—	min Finset instInsert LinearOrder.toDecidableEq instSingleton WithTop SemilatticeInf.toMin WithTop.semilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.some	—	min_insert min_singleton
min_singleton 📖	mathematical	—	min Finset instSingleton WithTop.some	—	instLawfulSingleton min_insert
min_union 📖	mathematical	—	min Finset instUnion LinearOrder.toDecidableEq WithTop SemilatticeInf.toMin WithTop.semilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	inf_union
notMem_of_coe_lt_min 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.some min	Finset instMembership	—	min_le LT.lt.not_ge
notMem_of_lt_min 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min WithTop.some	Finset instMembership	—	notMem_of_coe_lt_min LT.lt.trans_eq WithTop.coe_lt_coe
notMem_of_max_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder max WithBot.some	Finset instMembership	—	notMem_of_max_lt_coe Eq.trans_lt WithBot.coe_lt_coe
notMem_of_max_lt_coe 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder max WithBot.some	Finset instMembership	—	le_max LT.lt.not_ge
ofDual_max' 📖	mathematical	Nonempty OrderDual	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual max' OrderDual.instLinearOrder min' image LinearOrder.toDecidableEq Nonempty.image	—	Nonempty.image Nonempty.of_image sup'_congr inf'_congr inf'_image
ofDual_min' 📖	mathematical	Nonempty OrderDual	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual min' OrderDual.instLinearOrder max' image LinearOrder.toDecidableEq Nonempty.image	—	Nonempty.image Nonempty.of_image inf'_congr sup'_congr sup'_image
toDual_max' 📖	mathematical	Nonempty	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual max' min' OrderDual.instLinearOrder image OrderDual.instDecidableEq LinearOrder.toDecidableEq Nonempty.image	—	Nonempty.image Nonempty.of_image sup'_congr inf'_congr inf'_image
toDual_min' 📖	mathematical	Nonempty	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual min' max' OrderDual.instLinearOrder image OrderDual.instDecidableEq LinearOrder.toDecidableEq Nonempty.image	—	Nonempty.image Nonempty.of_image inf'_congr sup'_congr sup'_image

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_finset_max' 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset.Nonempty	Finset.max' Finset.image LinearOrder.toDecidableEq Finset.Nonempty.image	—	Finset.Nonempty.image Finset.max'_image
map_finset_min' 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset.Nonempty	Finset.min' Finset.image LinearOrder.toDecidableEq Finset.Nonempty.image	—	Finset.Nonempty.image Finset.min'_image

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_max_image 📖	mathematical	—	Multiset instMembership Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Finset.exists_max_image toFinset_nonempty mem_toFinset
exists_min_image 📖	mathematical	—	Multiset instMembership Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_max_image

---

← Back to Index