Documentation Verification Report

PFilter

📁 Source: Mathlib/Order/PFilter.lean

Statistics

Metric	Count
Definitions `IsPFilter`, `toPFilter`, `PFilter`, `dual`, `infGi`, `instInhabited`, `instOrderBot`, `instOrderTopOfOrderBot`, `instPartialOrder`, `instSetLike`, `principal`	11
Theorems `of_def`, `antitone_principal`, `directed`, `ext`, `ext_iff`, `inf_mem`, `inf_mem_iff`, `isPFilter`, `mem_mk`, `mem_of_le`, `mem_of_mem_of_le`, `mem_principal`, `nonempty`, `principal_le_iff`, `principal_le_principal_iff`, `sInf_gc`, `top_mem`	17
Total	28

Order

Definitions

Name	Category	Theorems
`IsPFilter` 📖	MathDef	5 math math: `IsPFilter.of_def`, `IdealFilter.isPFilter_gabrielComposition`, `Ideal.isPrime_iff`, `Ideal.IsPrime.compl_filter`, `PFilter.isPFilter`
`PFilter` 📖	CompData	20 math math: `Ideal.PrimePair.I_union_F`, `PFilter.ext_iff`, `PFilter.IsPrime.compl_ideal`, `PFilter.nonempty`, `Ideal.PrimePair.isCompl_I_F`, `Ideal.PrimePair.compl_I_eq_F`, `PFilter.antitone_principal`, `PFilter.inf_mem_iff`, `PFilter.directed`, `PFilter.sInf_gc`, `PFilter.isPrime_iff`, `PFilter.top_mem`, `PFilter.mem_mk`, `PFilter.isPFilter`, `PFilter.principal_le_iff`, `Ideal.PrimePair.F_union_I`, `PFilter.mem_principal`, `Ideal.PrimePair.disjoint`, `PFilter.principal_le_principal_iff`, `Ideal.PrimePair.compl_F_eq_I`

Order.IsPFilter

Definitions

Name	Category	Theorems
`toPFilter` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_def` 📖	mathematical	`Set.Nonempty` `DirectedOn` `Preorder.toLE` `Set` `Set.instMembership`	`Order.IsPFilter`	—	—

Order.PFilter

Definitions

Name	Category	Theorems
`dual` 📖	CompOp	—
`infGi` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instOrderBot` 📖	CompOp	—
`instOrderTopOfOrderBot` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	4 math math: `antitone_principal`, `sInf_gc`, `principal_le_iff`, `principal_le_principal_iff`
`instSetLike` 📖	CompOp	24 math math: `Order.Ideal.PrimePair.I_union_F`, `IdealFilter.ringFilterBasis_sets`, `WithIdealFilter.mem_nhds_zero_iff`, `IdealFilter.isPFilter_gabrielComposition`, `ext_iff`, `IsPrime.compl_ideal`, `nonempty`, `Order.Ideal.PrimePair.isCompl_I_F`, `Order.Ideal.PrimePair.compl_I_eq_F`, `inf_mem_iff`, `directed`, `sInf_gc`, `isPrime_iff`, `top_mem`, `mem_mk`, `isPFilter`, `principal_le_iff`, `Order.Ideal.PrimePair.F_union_I`, `WithIdealFilter.mem_nhds_iff`, `mem_principal`, `IdealFilter.isTorsionQuot_def`, `Order.Ideal.PrimePair.disjoint`, `Order.Ideal.PrimePair.compl_F_eq_I`, `IdealFilter.isUniform_iff_exists_ringFilterBasis`
`principal` 📖	CompOp	5 math math: `antitone_principal`, `sInf_gc`, `principal_le_iff`, `mem_principal`, `principal_le_principal_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_principal` 📖	mathematical	—	`Antitone` `Order.PFilter` `PartialOrder.toPreorder` `instPartialOrder` `principal`	—	`principal_le_principal_iff`
`directed` 📖	mathematical	—	`DirectedOn` `Preorder.toLE` `SetLike.coe` `Order.PFilter` `instSetLike`	—	`Order.Ideal.directed`
`ext` 📖	—	`SetLike.coe` `Order.PFilter` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `Order.PFilter` `instSetLike`	—	`ext`
`inf_mem` 📖	mathematical	`Order.PFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.instMembership` `instSetLike`	`SemilatticeInf.toMin`	—	`Order.Ideal.sup_mem`
`inf_mem_iff` 📖	mathematical	—	`Order.PFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.instMembership` `instSetLike` `SemilatticeInf.toMin`	—	`Order.Ideal.sup_mem_iff`
`isPFilter` 📖	mathematical	—	`Order.IsPFilter` `SetLike.coe` `Order.PFilter` `instSetLike`	—	`Order.Ideal.isIdeal`
`mem_mk` 📖	mathematical	—	`Order.PFilter` `SetLike.instMembership` `instSetLike` `OrderDual` `Order.Ideal` `OrderDual.instLE` `Preorder.toLE` `Order.Ideal.instSetLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`mem_of_le` 📖	—	`Preorder.toLE` `Order.PFilter` `SetLike.instMembership` `instSetLike`	—	—	`Order.Ideal.lower`
`mem_of_mem_of_le` 📖	—	`Order.PFilter` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—	—
`mem_principal` 📖	mathematical	—	`Order.PFilter` `SetLike.instMembership` `instSetLike` `principal` `Preorder.toLE`	—	—
`nonempty` 📖	mathematical	—	`Set.Nonempty` `SetLike.coe` `Order.PFilter` `instSetLike`	—	`Order.Ideal.nonempty`
`principal_le_iff` 📖	mathematical	—	`Order.PFilter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `principal` `SetLike.instMembership` `instSetLike`	—	`Order.Ideal.principal_le_iff`
`principal_le_principal_iff` 📖	mathematical	—	`Order.PFilter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `principal`	—	—
`sInf_gc` 📖	mathematical	—	`GaloisConnection` `OrderDual` `Order.PFilter` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `OrderDual.instPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `principal` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `SetLike.coe` `instSetLike` `OrderDual.ofDual`	—	`instIsConcreteLE`
`top_mem` 📖	mathematical	—	`Order.PFilter` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE`	—	`Order.Ideal.bot_mem`

---

← Back to Index