PrimeIdeal

📁 Source: Mathlib/Order/PrimeIdeal.lean

Statistics

Metric	Count
Definitions IsPrime, toPrimePair, PrimePair, F, I, IsPrime, toPrimePair	7
Theorems isPrime, compl_filter, compl_mem_of_notMem, isMaximal, mem_or_compl_mem, mem_or_mem, of_mem_or_mem, toIsProper, F_isPrime, F_union_I, I_isPrime, I_isProper, I_union_F, compl_F_eq_I, compl_I_eq_F, disjoint, isCompl_I_F, isPrime_iff, isPrime_iff_mem_or_compl_mem, isPrime_iff_mem_or_mem, isPrime_of_mem_or_compl_mem, compl_ideal, isPrime_iff	23
Total	30

Order.Ideal

Definitions

Name	Category	Theorems
IsPrime 📖	CompData	8 math math: isPrime_iff, IsMaximal.isPrime, isPrime_of_mem_or_compl_mem, DistribLattice.prime_ideal_of_disjoint_filter_ideal, isPrime_iff_mem_or_compl_mem, PrimePair.I_isPrime, isPrime_iff_mem_or_mem, IsPrime.of_mem_or_mem
PrimePair 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrime_iff 📖	mathematical	—	IsPrime IsProper Preorder.toLE Order.IsPFilter Compl.compl Set Set.instCompl SetLike.coe Order.Ideal instSetLike	—	—
isPrime_iff_mem_or_compl_mem 📖	mathematical	—	IsPrime PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Order.Ideal Preorder.toLE SetLike.instMembership instSetLike Compl.compl BooleanAlgebra.toCompl	—	IsPrime.mem_or_compl_mem isPrime_of_mem_or_compl_mem
isPrime_iff_mem_or_mem 📖	mathematical	—	IsPrime PartialOrder.toPreorder SemilatticeInf.toPartialOrder Order.Ideal Preorder.toLE SetLike.instMembership instSetLike	—	IsPrime.mem_or_mem IsPrime.of_mem_or_mem
isPrime_of_mem_or_compl_mem 📖	mathematical	Order.Ideal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra SetLike.instMembership instSetLike Compl.compl BooleanAlgebra.toCompl	IsPrime	—	sup_mem lower inf_le_right sup_inf_inf_compl inf_comm

Order.Ideal.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrime 📖	mathematical	—	Order.Ideal.IsPrime PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice	—	Order.Ideal.isPrime_iff_mem_or_mem toIsProper Mathlib.Tactic.Contrapose.contrapose₁ SemilatticeInf.instIsCodirectedOrder maximal_proper Order.Ideal.lt_sup_principal_of_notMem Set.eq_univ_iff_forall Order.Ideal.coe_sup_eq Order.Ideal.sup_mem Order.Ideal.lower le_inf le_sup_right

Order.Ideal.IsPrime

Definitions

Name	Category	Theorems
toPrimePair 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_filter 📖	mathematical	—	Order.IsPFilter Compl.compl Set Set.instCompl SetLike.coe Order.Ideal Preorder.toLE Order.Ideal.instSetLike	—	—
compl_mem_of_notMem 📖	mathematical	Order.Ideal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra SetLike.instMembership Order.Ideal.instSetLike	Compl.compl BooleanAlgebra.toCompl	—	mem_or_compl_mem
isMaximal 📖	mathematical	—	Order.Ideal.IsMaximal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra	—	Set.exists_of_ssubset Order.Ideal.sup_mem Order.Ideal.lower inf_le_right LT.lt.le compl_mem_of_notMem sup_inf_inf_compl
mem_or_compl_mem 📖	mathematical	—	Order.Ideal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra SetLike.instMembership Order.Ideal.instSetLike Compl.compl BooleanAlgebra.toCompl	—	mem_or_mem inf_compl_eq_bot Order.Ideal.bot_mem
mem_or_mem 📖	—	Order.Ideal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder SetLike.instMembership Order.Ideal.instSetLike SemilatticeInf.toMin	—	—	Mathlib.Tactic.Contrapose.contrapose₁ compl_filter Order.PFilter.inf_mem
of_mem_or_mem 📖	mathematical	Order.Ideal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder SetLike.instMembership Order.Ideal.instSetLike	Order.Ideal.IsPrime	—	Order.Ideal.isPrime_iff Order.IsPFilter.of_def Set.nonempty_compl Order.Ideal.isProper_iff inf_le_left inf_le_right Order.Ideal.mem_compl_of_ge
toIsProper 📖	mathematical	—	Order.Ideal.IsProper Preorder.toLE	—	—

Order.Ideal.PrimePair

Definitions

Name	Category	Theorems
F 📖	CompOp	7 math math: I_union_F, isCompl_I_F, F_isPrime, compl_I_eq_F, F_union_I, disjoint, compl_F_eq_I
I 📖	CompOp	8 math math: I_union_F, isCompl_I_F, compl_I_eq_F, F_union_I, I_isProper, I_isPrime, disjoint, compl_F_eq_I

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
F_isPrime 📖	mathematical	—	Order.PFilter.IsPrime F	—	compl_F_eq_I Order.Ideal.isIdeal
F_union_I 📖	mathematical	—	Set Set.instUnion SetLike.coe Order.PFilter Order.PFilter.instSetLike F Order.Ideal Preorder.toLE Order.Ideal.instSetLike I Set.univ	—	IsCompl.sup_eq_top IsCompl.symm isCompl_I_F
I_isPrime 📖	mathematical	—	Order.Ideal.IsPrime I	—	I_isProper compl_I_eq_F Order.PFilter.isPFilter
I_isProper 📖	mathematical	—	Order.Ideal.IsProper Preorder.toLE I	—	Order.PFilter.nonempty Order.Ideal.isProper_of_notMem compl_I_eq_F
I_union_F 📖	mathematical	—	Set Set.instUnion SetLike.coe Order.Ideal Preorder.toLE Order.Ideal.instSetLike I Order.PFilter Order.PFilter.instSetLike F Set.univ	—	IsCompl.sup_eq_top isCompl_I_F
compl_F_eq_I 📖	mathematical	—	Compl.compl Set Set.instCompl SetLike.coe Order.PFilter Order.PFilter.instSetLike F Order.Ideal Preorder.toLE Order.Ideal.instSetLike I	—	IsCompl.eq_compl isCompl_I_F
compl_I_eq_F 📖	mathematical	—	Compl.compl Set Set.instCompl SetLike.coe Order.Ideal Preorder.toLE Order.Ideal.instSetLike I Order.PFilter Order.PFilter.instSetLike F	—	IsCompl.compl_eq isCompl_I_F
disjoint 📖	mathematical	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Order.Ideal Preorder.toLE Order.Ideal.instSetLike I Order.PFilter Order.PFilter.instSetLike F	—	IsCompl.disjoint isCompl_I_F
isCompl_I_F 📖	mathematical	—	IsCompl Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instBoundedOrder SetLike.coe Order.Ideal Preorder.toLE Order.Ideal.instSetLike I Order.PFilter Order.PFilter.instSetLike F	—	—

Order.PFilter

Definitions

Name	Category	Theorems
IsPrime 📖	CompData	2 math math: Order.Ideal.PrimePair.F_isPrime, isPrime_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrime_iff 📖	mathematical	—	IsPrime Order.IsIdeal Preorder.toLE Compl.compl Set Set.instCompl SetLike.coe Order.PFilter instSetLike	—	—

Order.PFilter.IsPrime

Definitions

Name	Category	Theorems
toPrimePair 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_ideal 📖	mathematical	—	Order.IsIdeal Preorder.toLE Compl.compl Set Set.instCompl SetLike.coe Order.PFilter Order.PFilter.instSetLike	—	—

---

← Back to Index