Minimal

📁 Source: Mathlib/Order/Minimal.lean

Statistics

Metric	Count
Definitions Minimal, Minimal, mapSetOfMaximal, mapSetOfMinimal, setOfMaximalIsoSetOfMinimal, setOfMinimalIsoSetOfMaximal	6
Theorems maximal, maximal_iff, minimal, minimal_iff, and_left, and_right, dual, eq_of_ge, eq_of_le, eq_of_subset, eq_of_superset, le, mem_of_prop_insert, mono, not_gt, not_prop_of_gt, not_prop_of_ssuperset, not_ssuperset, of_dual, or, anti, le, maximal_of_strictMonoOn, minimalFor_of_strictAntiOn_comp, minimal_of_strictAntiOn, not_gt, not_prop_of_gt, of_strictMonoOn_comp, and_left, and_right, dual, eq_of_ge, eq_of_le, eq_of_subset, eq_of_superset, le, mono, notMem_of_prop_diff_singleton, not_lt, not_prop_of_lt, not_prop_of_ssubset, not_ssubset, of_dual, or, anti, le, maximalFor_of_strictAntiOn_comp, maximal_of_strictAntiOn, minimal_of_strictMonoOn, not_lt, not_prop_of_lt, of_strictMonoOn_comp, image_setOf_maximal, image_setOf_minimal, inter_preimage_setOf_maximal_eq_of_subset, inter_preimage_setOf_minimal_eq_of_subset, maximal_apply_iff, maximal_apply_mem_inter_range_iff, maximal_mem_image, maximal_mem_image_iff, minimal_apply_mem_iff, minimal_apply_mem_inter_range_iff, minimal_mem_image, minimal_mem_image_iff, image_setOf_maximal, image_setOf_minimal, map_maximal_mem, map_minimal_mem, maximal_mem_iff, minimal_mem_iff, exists_diff_singleton_of_not_minimal, exists_insert_of_not_maximal, maximal_iff_forall_insert, maximal_iff_forall_ssuperset, minimal_iff_forall_diff_singleton, minimal_iff_forall_ssubset, exists_gt_of_not_maximal, exists_lt_of_not_minimal, exists_maximalFor_of_wellFoundedGT, exists_maximal_ge_of_wellFoundedGT, exists_maximal_of_wellFoundedGT, exists_minimalFor_of_wellFoundedLT, exists_minimal_le_of_wellFoundedLT, exists_minimal_of_wellFoundedLT, image_antitone_setOf_maximal, image_antitone_setOf_maximal_mem, image_antitone_setOf_minimal, image_antitone_setOf_minimal_mem, image_monotone_setOf_maximal, image_monotone_setOf_maximal_mem, image_monotone_setOf_minimal, image_monotone_setOf_minimal_mem, maximalFor_eq_iff, maximalFor_id, maximalFor_iff_forall_gt, maximal_and_iff_left_of_imp, maximal_and_iff_right_of_imp, maximal_eq_iff, maximal_false, maximal_ge_iff, maximal_gt_iff, maximal_iff, maximal_iff_eq, maximal_iff_forall_gt, maximal_iff_isMax, maximal_iff_maximal_of_imp_of_forall, maximal_le_iff, maximal_maximal, maximal_mem_Icc, maximal_mem_Ioc, maximal_mem_iff, maximal_mem_image_antitone, maximal_mem_image_antitone_iff, maximal_mem_image_monotone, maximal_mem_image_monotone_iff, maximal_subset_iff, maximal_subset_iff', maximal_subtype, maximal_toDual, maximal_true, maximal_true_subtype, minimalFor_eq_iff, minimalFor_id, minimalFor_iff_forall_lt, minimal_and_iff_left_of_imp, minimal_and_iff_right_of_imp, minimal_eq_iff, minimal_false, minimal_ge_iff, minimal_iff, minimal_iff_eq, minimal_iff_forall_lt, minimal_iff_isMin, minimal_iff_minimal_of_imp_of_forall, minimal_le_iff, minimal_lt_iff, minimal_mem_Icc, minimal_mem_Ico, minimal_mem_iff, minimal_mem_image_antitone, minimal_mem_image_antitone_iff, minimal_mem_image_monotone, minimal_mem_image_monotone_iff, minimal_minimal, minimal_subset_iff, minimal_subset_iff', minimal_subtype, minimal_toDual, minimal_true, minimal_true_subtype, not_maximal_iff, not_maximal_iff_exists_gt, not_maximal_subset_iff, not_minimal_iff, not_minimal_iff_exists_lt, not_minimal_subset_iff, setOf_maximal_subset, setOf_minimal_subset	158
Total	164

Fermat42

Definitions

Name	Category	Theorems
Minimal 📖	MathDef	3 math math: exists_pos_odd_minimal, exists_odd_minimal, exists_minimal

IsGreatest

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maximal 📖	mathematical	IsGreatest Preorder.toLE	Maximal Set Set.instMembership	—	—
maximal_iff 📖	mathematical	IsGreatest Preorder.toLE PartialOrder.toPreorder	Maximal Set Set.instMembership	—	Maximal.eq_of_le Maximal.prop maximal

IsLeast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
minimal 📖	mathematical	IsLeast Preorder.toLE	Minimal Set Set.instMembership	—	—
minimal_iff 📖	mathematical	IsLeast Preorder.toLE PartialOrder.toPreorder	Minimal Set Set.instMembership	—	Minimal.eq_of_ge Minimal.prop minimal

Maximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and_left 📖	—	Maximal	—	—	mono prop
and_right 📖	—	Maximal	—	—	mono prop
dual 📖	mathematical	Minimal	Maximal OrderDual OrderDual.instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual	—	maximal_toDual
eq_of_ge 📖	—	Maximal Preorder.toLE PartialOrder.toPreorder	—	—	eq_of_le
eq_of_le 📖	—	Maximal Preorder.toLE PartialOrder.toPreorder	—	—	LE.le.antisymm
eq_of_subset 📖	—	Maximal Set Set.instLE Set.instHasSubset	—	—	eq_of_le
eq_of_superset 📖	—	Maximal Set Set.instLE Set.instHasSubset	—	—	eq_of_ge
le 📖	—	Maximal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	le_of_not_gt not_gt
mem_of_prop_insert 📖	mathematical	Maximal Set Set.instLE Set.instInsert	Set.instMembership	—	Set.mem_insert eq_of_subset Set.subset_insert
mono 📖	—	Maximal Pi.hasLe Prop.le	—	—	le_of_ge
not_gt 📖	mathematical	Maximal Preorder.toLE	Preorder.toLT	—	not_prop_of_gt
not_prop_of_gt 📖	—	Maximal Preorder.toLE Preorder.toLT	—	—	maximal_iff_forall_gt
not_prop_of_ssuperset 📖	—	Maximal Set Set.instLE Set.instHasSSubset	—	—	maximal_iff_forall_gt
not_ssuperset 📖	mathematical	Maximal Set Set.instLE	Set.instHasSSubset	—	not_gt
of_dual 📖	mathematical	Maximal OrderDual OrderDual.instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual	Minimal	—	maximal_toDual
or 📖	—	Maximal	—	—	Minimal.or

MaximalFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anti 📖	—	MaximalFor Pi.hasLe Prop.le	—	—	le_of_le
le 📖	—	MaximalFor Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	le_of_not_gt not_gt
maximal_of_strictMonoOn 📖	mathematical	StrictMonoOn setOf MaximalFor Preorder.toLE	Maximal	—	maximalFor_id of_strictMonoOn_comp Set.image_id
minimalFor_of_strictAntiOn_comp 📖	mathematical	StrictAntiOn Set.image setOf MaximalFor Preorder.toLE	MinimalFor	—	prop not_gt lt_of_le_not_ge
minimal_of_strictAntiOn 📖	mathematical	StrictAntiOn setOf MaximalFor Preorder.toLE	Minimal	—	minimalFor_id minimalFor_of_strictAntiOn_comp Set.image_id
not_gt 📖	mathematical	MaximalFor Preorder.toLE	Preorder.toLT	—	not_prop_of_gt
not_prop_of_gt 📖	—	MaximalFor Preorder.toLE Preorder.toLT	—	—	maximalFor_iff_forall_gt
of_strictMonoOn_comp 📖	—	StrictMonoOn Set.image setOf MaximalFor Preorder.toLE	—	—	prop not_gt lt_of_le_not_ge

Minimal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and_left 📖	—	Minimal	—	—	mono prop
and_right 📖	—	Minimal	—	—	mono prop
dual 📖	mathematical	Maximal	Minimal OrderDual OrderDual.instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual	—	minimal_toDual
eq_of_ge 📖	—	Minimal Preorder.toLE PartialOrder.toPreorder	—	—	LE.le.antisymm
eq_of_le 📖	—	Minimal Preorder.toLE PartialOrder.toPreorder	—	—	eq_of_ge
eq_of_subset 📖	—	Minimal Set Set.instLE Set.instHasSubset	—	—	eq_of_le
eq_of_superset 📖	—	Minimal Set Set.instLE Set.instHasSubset	—	—	eq_of_ge
le 📖	—	Minimal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	le_of_not_gt not_lt
mono 📖	—	Minimal Pi.hasLe Prop.le	—	—	le_of_le
notMem_of_prop_diff_singleton 📖	mathematical	Minimal Set Set.instLE Set.instSDiff Set.instSingletonSet	Set.instMembership	—	Eq.subset Set.instReflSubset eq_of_superset Set.diff_subset
not_lt 📖	mathematical	Minimal Preorder.toLE	Preorder.toLT	—	not_prop_of_lt
not_prop_of_lt 📖	—	Minimal Preorder.toLE Preorder.toLT	—	—	minimal_iff_forall_lt
not_prop_of_ssubset 📖	—	Minimal Set Set.instLE Set.instHasSSubset	—	—	minimal_iff_forall_lt
not_ssubset 📖	mathematical	Minimal Set Set.instLE	Set.instHasSSubset	—	not_lt
of_dual 📖	mathematical	Minimal OrderDual OrderDual.instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual	Maximal	—	minimal_toDual
or 📖	—	Minimal	—	—	—

MinimalFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anti 📖	—	MinimalFor Pi.hasLe Prop.le	—	—	le_of_le
le 📖	—	MinimalFor Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	le_of_not_gt not_lt
maximalFor_of_strictAntiOn_comp 📖	mathematical	StrictAntiOn Set.image setOf MinimalFor Preorder.toLE	MaximalFor	—	prop not_lt lt_of_le_not_ge
maximal_of_strictAntiOn 📖	mathematical	StrictAntiOn setOf MinimalFor Preorder.toLE	Maximal	—	maximalFor_id maximalFor_of_strictAntiOn_comp Set.image_id
minimal_of_strictMonoOn 📖	mathematical	StrictMonoOn setOf MinimalFor Preorder.toLE	Minimal	—	minimalFor_id of_strictMonoOn_comp Set.image_id
not_lt 📖	mathematical	MinimalFor Preorder.toLE	Preorder.toLT	—	not_prop_of_lt
not_prop_of_lt 📖	—	MinimalFor Preorder.toLE Preorder.toLT	—	—	minimalFor_iff_forall_lt
of_strictMonoOn_comp 📖	—	StrictMonoOn Set.image setOf MinimalFor Preorder.toLE	—	—	prop not_lt lt_of_le_not_ge

OrderEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_setOf_maximal 📖	mathematical	—	Set.image DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding setOf Maximal Set Set.instMembership	—	image_monotone_setOf_maximal le_iff_le
image_setOf_minimal 📖	mathematical	—	Set.image DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding setOf Minimal Set Set.instMembership	—	image_monotone_setOf_minimal le_iff_le
inter_preimage_setOf_maximal_eq_of_subset 📖	mathematical	Set Set.instHasSubset Set.image DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding	Set.instMembership Set.instInter Set.preimage setOf Maximal	—	inter_preimage_setOf_minimal_eq_of_subset
inter_preimage_setOf_minimal_eq_of_subset 📖	mathematical	Set Set.instHasSubset Set.image DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding	Set.instMembership Set.instInter Set.preimage setOf Minimal	—	minimal_apply_mem_iff HasSubset.Subset.trans Set.instIsTransSubset Set.image_subset_range minimal_and_iff_left_of_imp Function.Injective.mem_set_image RelEmbedding.injective
maximal_apply_iff 📖	mathematical	Set Set.instHasSubset Set.range DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding	Maximal Set.instMembership	—	minimal_apply_mem_iff
maximal_apply_mem_inter_range_iff 📖	mathematical	—	Maximal Preorder.toLE Set Set.instMembership Set.instInter Set.range DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding	—	minimal_apply_mem_inter_range_iff
maximal_mem_image 📖	mathematical	Maximal Preorder.toLE Set Set.instMembership	Set.image DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding	—	maximal_mem_image_monotone le_iff_le
maximal_mem_image_iff 📖	mathematical	Set Set.instMembership	Maximal Preorder.toLE Set.image DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding	—	maximal_mem_image_monotone_iff le_iff_le
minimal_apply_mem_iff 📖	mathematical	Set Set.instHasSubset Set.range DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding	Minimal Set.instMembership	—	minimal_apply_mem_inter_range_iff Set.inter_eq_self_of_subset_left
minimal_apply_mem_inter_range_iff 📖	mathematical	—	Minimal Preorder.toLE Set Set.instMembership Set.instInter Set.range DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding	—	Minimal.prop le_iff_le Minimal.le_of_le RelEmbedding.instEmbeddingLike
minimal_mem_image 📖	mathematical	Minimal Preorder.toLE Set Set.instMembership	Set.image DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding	—	minimal_mem_image_monotone le_iff_le
minimal_mem_image_iff 📖	mathematical	Set Set.instMembership	Minimal Preorder.toLE Set.image DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding	—	minimal_mem_image_monotone_iff le_iff_le

OrderIso

Definitions

Name	Category	Theorems
mapSetOfMaximal 📖	CompOp	—
mapSetOfMinimal 📖	CompOp	—
setOfMaximalIsoSetOfMinimal 📖	CompOp	—
setOfMinimalIsoSetOfMaximal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_setOf_maximal 📖	mathematical	—	Set.image DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso setOf Maximal symm	—	apply_symm_apply symm_apply_apply image_monotone_setOf_maximal le_iff_le
image_setOf_minimal 📖	mathematical	—	Set.image DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso setOf Minimal symm	—	apply_symm_apply symm_apply_apply image_monotone_setOf_minimal le_iff_le
map_maximal_mem 📖	mathematical	Maximal Preorder.toLE Set Set.instMembership	DFunLike.coe OrderIso Set.Elem instFunLikeOrderIso Maximal.prop	—	Maximal.prop EquivLike.range_comp Subtype.range_coe_subtype Set.image_univ OrderEmbedding.maximal_mem_image
map_minimal_mem 📖	mathematical	Minimal Preorder.toLE Set Set.instMembership	DFunLike.coe OrderIso Set.Elem instFunLikeOrderIso Minimal.prop	—	Minimal.prop EquivLike.range_comp Subtype.range_coe_subtype Set.image_univ OrderEmbedding.minimal_mem_image

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_diff_singleton_of_not_minimal 📖	mathematical	Minimal Set instLE	instMembership instSDiff instSingletonSet	—	minimal_iff_forall_diff_singleton
exists_insert_of_not_maximal 📖	mathematical	Maximal Set instLE	instMembership instInsert	—	maximal_iff_forall_insert
maximal_iff_forall_insert 📖	mathematical	—	Maximal Set instLE instInsert	—	Maximal.mem_of_prop_insert insert_subset
maximal_iff_forall_ssuperset 📖	mathematical	—	Maximal Set instLE	—	maximal_iff_forall_gt
minimal_iff_forall_diff_singleton 📖	mathematical	—	Minimal Set instLE instSDiff instSingletonSet	—	Minimal.notMem_of_prop_diff_singleton by_contra subset_diff_singleton
minimal_iff_forall_ssubset 📖	mathematical	—	Minimal Set instLE	—	minimal_iff_forall_lt

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maximal_mem_iff 📖	mathematical	Set.Subsingleton	Maximal Preorder.toLE Set Set.instMembership	—	eq_empty_or_singleton
minimal_mem_iff 📖	mathematical	Set.Subsingleton	Minimal Preorder.toLE Set Set.instMembership	—	eq_empty_or_singleton

(root)

Definitions

Name	Category	Theorems
Minimal 📖	MathDef	85 math math: Set.minimal_iff_forall_ssubset, Maximal.of_dual, Matroid.isCocircuit_iff_minimal_compl_nonspanning, image_monotone_setOf_minimal, minimal_ge_iff, minimalPrimes_eq_minimals, Matroid.IsCircuit.minimal, minimal_iff_minimal_of_imp_of_forall, minimal_mem_image_antitone_iff, not_minimal_iff_exists_lt, maximal_mem_image_antitone_iff, minimal_le_iff, Set.IsPWO.exists_le_minimal, minimal_mem_Ico, MinimalFor.minimal_of_strictMonoOn, IsLeast.minimal_iff, OrderEmbedding.inter_preimage_setOf_minimal_eq_of_subset, minimal_subset_iff', exists_minimal_le_of_wellFoundedLT, SimpleGraph.isTree_iff_minimal_connected, Finset.exists_minimal, IsAntichain.minimal_mem_iff, minimal_minimal, Set.minimal_iff_forall_diff_singleton, not_minimal_iff, Finset.minimal_iff_forall_diff_singleton, minimal_and_iff_left_of_imp, Finset.exists_le_minimal, maximal_mem_image_antitone, IsLeast.minimal, minimal_mem_image_monotone_iff, Set.IsPWO.exists_minimal, Submonoid.exists_minimal_closure_eq_top, minimal_toDual, AddSubmonoid.exists_minimal_closure_eq_top, minimal_iff_isLeast, minimal_false, not_minimal_subset_iff, minimal_iff_eq, OrderIso.image_setOf_minimal, MaximalFor.minimal_of_strictAntiOn, IsAntichain.minimal_mem_upperClosure_iff_mem, maximal_toDual, minimal_mem_iff, minimal_subset_iff, OrderEmbedding.minimal_apply_mem_iff, image_antitone_setOf_maximal_mem, exists_minimal_of_wellFoundedLT, minimalFor_id, minimal_iff, minimal_iff_forall_lt, OrderEmbedding.image_setOf_minimal, Matroid.isCircuit_def, zorn_superset_nonempty, setOf_minimal_subset, image_antitone_setOf_minimal_mem, OrderEmbedding.minimal_mem_image_iff, Set.Finite.exists_minimal, zorn_superset, OrderEmbedding.minimal_apply_mem_inter_range_iff, Matroid.isCocircuit_iff_minimal, minimal_eq_iff, Finite.exists_le_minimal, minimal_lt_iff, image_monotone_setOf_minimal_mem, image_antitone_setOf_minimal, Matroid.isCircuit_iff_minimal_not_indep, AddSubmonoid.FG.exists_minimal_closure_eq, setOf_minimal_antichain, Matroid.isBase_iff_minimal_spanning, Set.Finite.exists_le_minimal, Matroid.isCocircuit_iff_minimal_compl_nonspanning', image_antitone_setOf_maximal, minimal_true, minimal_and_iff_right_of_imp, Matroid.IsCircuit.minimal_not_indep, minimal_subtype, Set.Subsingleton.minimal_mem_iff, minimal_true_subtype, Submonoid.FG.exists_minimal_closure_eq, minimal_mem_Icc, Order.height_eq_coe_iff_minimal_le_height, Minimal.dual, minimal_iff_isMin, DirectedOn.minimal_iff_isLeast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_gt_of_not_maximal 📖	mathematical	Maximal Preorder.toLE	Preorder.toLT	—	not_maximal_iff_exists_gt
exists_lt_of_not_minimal 📖	mathematical	Minimal Preorder.toLE	Preorder.toLT	—	not_minimal_iff_exists_lt
exists_maximalFor_of_wellFoundedGT 📖	mathematical	—	MaximalFor Preorder.toLE	—	exists_minimalFor_of_wellFoundedLT instWellFoundedLTOrderDualOfWellFoundedGT
exists_maximal_ge_of_wellFoundedGT 📖	mathematical	—	Preorder.toLE Maximal	—	exists_minimal_le_of_wellFoundedLT instWellFoundedLTOrderDualOfWellFoundedGT
exists_maximal_of_wellFoundedGT 📖	mathematical	—	Maximal Preorder.toLE	—	exists_minimal_of_wellFoundedLT instWellFoundedLTOrderDualOfWellFoundedGT
exists_minimalFor_of_wellFoundedLT 📖	mathematical	—	MinimalFor Preorder.toLE	—	WellFounded.has_min IsWellFounded.wf instIsWellFoundedInvImage
exists_minimal_le_of_wellFoundedLT 📖	mathematical	—	Preorder.toLE Minimal	—	exists_minimal_of_wellFoundedLT le_rfl LE.le.trans
exists_minimal_of_wellFoundedLT 📖	mathematical	—	Minimal Preorder.toLE	—	exists_minimalFor_of_wellFoundedLT
image_antitone_setOf_maximal 📖	mathematical	Preorder.toLE	Set.image setOf Maximal Minimal	—	image_monotone_setOf_maximal
image_antitone_setOf_maximal_mem 📖	mathematical	Preorder.toLE	Set.image setOf Maximal Set Set.instMembership Minimal	—	image_antitone_setOf_maximal
image_antitone_setOf_minimal 📖	mathematical	Preorder.toLE	Set.image setOf Minimal Maximal	—	image_monotone_setOf_minimal
image_antitone_setOf_minimal_mem 📖	mathematical	Preorder.toLE	Set.image setOf Minimal Set Set.instMembership Maximal	—	image_antitone_setOf_minimal
image_monotone_setOf_maximal 📖	mathematical	Preorder.toLE	Set.image setOf Maximal	—	image_monotone_setOf_minimal
image_monotone_setOf_maximal_mem 📖	mathematical	Preorder.toLE	Set.image setOf Maximal Set Set.instMembership	—	image_monotone_setOf_maximal
image_monotone_setOf_minimal 📖	mathematical	Preorder.toLE	Set.image setOf Minimal	—	Set.ext minimal_mem_image_monotone_iff Minimal.prop Set.mem_setOf_eq Set.mem_image_of_mem
image_monotone_setOf_minimal_mem 📖	mathematical	Preorder.toLE	Set.image setOf Minimal Set Set.instMembership	—	image_monotone_setOf_minimal
maximalFor_eq_iff 📖	mathematical	—	MaximalFor	—	—
maximalFor_id 📖	mathematical	—	MaximalFor Maximal	—	—
maximalFor_iff_forall_gt 📖	mathematical	—	MaximalFor Preorder.toLE	—	minimalFor_iff_forall_lt
maximal_and_iff_left_of_imp 📖	mathematical	—	Maximal	—	minimal_and_iff_left_of_imp
maximal_and_iff_right_of_imp 📖	mathematical	—	Maximal	—	minimal_and_iff_right_of_imp
maximal_eq_iff 📖	mathematical	—	Maximal	—	—
maximal_false 📖	mathematical	—	Maximal	—	instIsEmptyFalse
maximal_ge_iff 📖	mathematical	—	Maximal Preorder.toLE IsMax	—	minimal_le_iff
maximal_gt_iff 📖	mathematical	—	Maximal Preorder.toLE Preorder.toLT IsMax	—	minimal_lt_iff
maximal_iff 📖	mathematical	—	Maximal Preorder.toLE PartialOrder.toPreorder	—	minimal_iff
maximal_iff_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Maximal	—	minimal_iff_eq
maximal_iff_forall_gt 📖	mathematical	—	Maximal Preorder.toLE	—	minimal_iff_forall_lt
maximal_iff_isMax 📖	mathematical	—	Maximal IsMax	—	Maximal.prop Maximal.le_of_ge
maximal_iff_maximal_of_imp_of_forall 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Maximal	—	minimal_iff_minimal_of_imp_of_forall
maximal_le_iff 📖	mathematical	—	Maximal Preorder.toLE PartialOrder.toPreorder	—	maximal_iff_eq Eq.le
maximal_maximal 📖	mathematical	—	Maximal	—	minimal_minimal
maximal_mem_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Maximal Set Set.instMembership Set.Icc	—	maximal_iff_eq Eq.le
maximal_mem_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Maximal Preorder.toLE Set Set.instMembership Set.Ioc	—	maximal_iff_eq Eq.le
maximal_mem_iff 📖	mathematical	—	Maximal Preorder.toLE PartialOrder.toPreorder Set Set.instMembership	—	maximal_iff
maximal_mem_image_antitone 📖	mathematical	Preorder.toLE Maximal Set Set.instMembership	Minimal Set.image	—	maximal_mem_image_monotone
maximal_mem_image_antitone_iff 📖	mathematical	Set Set.instMembership Preorder.toLE	Maximal Set.image Minimal	—	minimal_mem_image_monotone_iff
maximal_mem_image_monotone 📖	mathematical	Preorder.toLE Maximal Set Set.instMembership	Set.image	—	minimal_mem_image_monotone
maximal_mem_image_monotone_iff 📖	mathematical	Set Set.instMembership Preorder.toLE	Maximal Set.image	—	minimal_mem_image_monotone_iff
maximal_subset_iff 📖	mathematical	—	Maximal Set Set.instLE	—	maximal_iff
maximal_subset_iff' 📖	mathematical	—	Maximal Set Set.instLE Set.instHasSubset	—	—
maximal_subtype 📖	mathematical	—	Maximal Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Prop.instBooleanAlgebra	—	minimal_subtype
maximal_toDual 📖	mathematical	—	Maximal OrderDual OrderDual.instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual Minimal	—	—
maximal_true 📖	mathematical	—	Maximal IsMax	—	minimal_true
maximal_true_subtype 📖	mathematical	—	Maximal	—	—
minimalFor_eq_iff 📖	mathematical	—	MinimalFor	—	—
minimalFor_id 📖	mathematical	—	MinimalFor Minimal	—	—
minimalFor_iff_forall_lt 📖	mathematical	—	MinimalFor Preorder.toLE	—	—
minimal_and_iff_left_of_imp 📖	mathematical	—	Minimal	—	minimal_and_iff_right_of_imp
minimal_and_iff_right_of_imp 📖	mathematical	—	Minimal	—	Minimal.prop
minimal_eq_iff 📖	mathematical	—	Minimal	—	—
minimal_false 📖	mathematical	—	Minimal	—	instIsEmptyFalse
minimal_ge_iff 📖	mathematical	—	Minimal Preorder.toLE PartialOrder.toPreorder	—	minimal_iff_eq Eq.le
minimal_iff 📖	mathematical	—	Minimal Preorder.toLE PartialOrder.toPreorder	—	Minimal.eq_of_ge Eq.le
minimal_iff_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Minimal	—	Minimal.eq_of_ge Minimal.prop
minimal_iff_forall_lt 📖	mathematical	—	Minimal Preorder.toLE	—	—
minimal_iff_isMin 📖	mathematical	—	Minimal IsMin	—	Minimal.prop Minimal.le_of_le
minimal_iff_minimal_of_imp_of_forall 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Minimal	—	Minimal.prop LE.le.antisymm Minimal.le_of_le LE.le.trans
minimal_le_iff 📖	mathematical	—	Minimal Preorder.toLE IsMin	—	minimal_iff_isMin LE.le.trans
minimal_lt_iff 📖	mathematical	—	Minimal Preorder.toLE Preorder.toLT IsMin	—	minimal_iff_isMin LE.le.trans_lt
minimal_mem_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Minimal Set Set.instMembership Set.Icc	—	minimal_iff_eq Eq.le
minimal_mem_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Minimal Preorder.toLE Set Set.instMembership Set.Ico	—	minimal_iff_eq Eq.le
minimal_mem_iff 📖	mathematical	—	Minimal Preorder.toLE PartialOrder.toPreorder Set Set.instMembership	—	minimal_iff
minimal_mem_image_antitone 📖	mathematical	Preorder.toLE Minimal Set Set.instMembership	Maximal Set.image	—	minimal_mem_image_monotone
minimal_mem_image_antitone_iff 📖	mathematical	Set Set.instMembership Preorder.toLE	Minimal Set.image Maximal	—	maximal_mem_image_monotone_iff
minimal_mem_image_monotone 📖	mathematical	Preorder.toLE Minimal Set Set.instMembership	Set.image	—	Set.mem_image_of_mem Minimal.prop Minimal.le_of_le
minimal_mem_image_monotone_iff 📖	mathematical	Set Set.instMembership Preorder.toLE	Minimal Set.image	—	Minimal.le_of_le Set.mem_image_of_mem minimal_mem_image_monotone
minimal_minimal 📖	mathematical	—	Minimal	—	Minimal.prop Minimal.le_of_le
minimal_subset_iff 📖	mathematical	—	Minimal Set Set.instLE	—	minimal_iff
minimal_subset_iff' 📖	mathematical	—	Minimal Set Set.instLE Set.instHasSubset	—	—
minimal_subtype 📖	mathematical	—	Minimal Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Prop.instBooleanAlgebra	—	—
minimal_toDual 📖	mathematical	—	Minimal OrderDual OrderDual.instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual Maximal	—	—
minimal_true 📖	mathematical	—	Minimal IsMin	—	—
minimal_true_subtype 📖	mathematical	—	Minimal	—	—
not_maximal_iff 📖	mathematical	—	Maximal	—	not_minimal_iff
not_maximal_iff_exists_gt 📖	mathematical	—	Maximal Preorder.toLE Preorder.toLT	—	not_minimal_iff_exists_lt
not_maximal_subset_iff 📖	mathematical	—	Maximal Set Set.instLE Set.instHasSSubset	—	not_maximal_iff_exists_gt
not_minimal_iff 📖	mathematical	—	Minimal	—	—
not_minimal_iff_exists_lt 📖	mathematical	—	Minimal Preorder.toLE Preorder.toLT	—	not_minimal_iff
not_minimal_subset_iff 📖	mathematical	—	Minimal Set Set.instLE Set.instHasSSubset	—	not_minimal_iff_exists_lt
setOf_maximal_subset 📖	mathematical	—	Set Set.instHasSubset setOf Maximal Preorder.toLE Set.instMembership	—	Set.sep_subset
setOf_minimal_subset 📖	mathematical	—	Set Set.instHasSubset setOf Minimal Preorder.toLE Set.instMembership	—	Set.sep_subset

---

← Back to Index