PrimeSeparator

📁 Source: Mathlib/Order/PrimeSeparator.lean

Statistics

Metric	Count
Definitions	0
Theorems mem_ideal_sup_principal, prime_ideal_of_disjoint_filter_ideal	2
Total	2

DistribLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_ideal_sup_principal 📖	mathematical	—	Order.Ideal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf toLattice SetLike.instMembership Order.Ideal.instSetLike Order.Ideal.instMax Lattice.toSemilatticeSup OrderBot.instIsCodirectedOrder SemilatticeSup.toPartialOrder BoundedOrder.toOrderBot Order.Ideal.principal SemilatticeSup.toMax	—	OrderBot.instIsCodirectedOrder le_trans sup_le_sup_left le_refl
prime_ideal_of_disjoint_filter_ideal 📖	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.PFilter PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf toLattice Order.PFilter.instSetLike Order.Ideal Preorder.toLE Order.Ideal.instSetLike	Order.Ideal.IsPrime Order.Ideal.instPartialOrderIdeal	—	Order.Ideal.isIdeal le_refl Order.isIdeal_sUnion_of_isChain le_trans le_sSup zorn_subset_nonempty Maximal.prop Order.Ideal.isProper_of_notMem Set.disjoint_left Order.PFilter.top_mem Order.Ideal.isPrime_iff_mem_or_mem Mathlib.Tactic.Contrapose.contrapose₁ OrderBot.instIsCodirectedOrder Set.mem_of_subset_of_mem le_sup_right Order.Ideal.mem_principal_self Maximal.eq_of_le le_sup_left instIsConcreteLE Set.not_disjoint_iff mem_ideal_sup_principal Order.Ideal.sup_mem inf_le_inf sup_le_sup sup_inf_left Order.PFilter.mem_of_le Order.PFilter.inf_mem Mathlib.Tactic.Contrapose.contrapose₃

---

← Back to Index