Documentation Verification Report

HullKernel

📁 Source: Mathlib/Topology/Order/HullKernel.lean

Statistics

Metric	Count
Definitions `OrderGenerates`, `gi`, `hull`, `kernel`	4
Theorems `closedsGC_closureOperator`, `gc`, `gc_closureOperator`, `hull_finsetInf`, `hull_iSup`, `hull_inf`, `hull_kernel_of_isClosed`, `hull_sSup`, `isClosed_iff`, `isOpen_iff`, `isTopologicalBasis_relativeLower`, `kernel_hull`, `preimage_upperClosure_compl_finset`	13
Total	17

PrimitiveSpectrum

Definitions

Name	Category	Theorems
`OrderGenerates` 📖	MathDef	—
`gi` 📖	CompOp	—
`hull` 📖	CompOp	13 math math: `isTopologicalBasis_relativeLower`, `hull_kernel_of_isClosed`, `hull_inf`, `hull_finsetInf`, `gc_closureOperator`, `preimage_upperClosure_compl_finset`, `closedsGC_closureOperator`, `isOpen_iff`, `kernel_hull`, `isClosed_iff`, `hull_sSup`, `hull_iSup`, `gc`
`kernel` 📖	CompOp	5 math math: `hull_kernel_of_isClosed`, `gc_closureOperator`, `closedsGC_closureOperator`, `kernel_hull`, `gc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedsGC_closureOperator` 📖	mathematical	`InfPrime` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `OrderGenerates`	`DFunLike.coe` `ClosureOperator` `Set` `Set.Elem` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `GaloisConnection.closureOperator` `TopologicalSpace.Closeds` `instTopologicalSpaceSubtype` `Set.instMembership` `TopologicalSpace.Closeds.instPartialOrder` `TopologicalSpace.Closeds.closure` `SetLike.coe` `TopologicalSpace.Closeds.instSetLike` `TopologicalSpace.Closeds.gc` `hull` `kernel`	—	`TopologicalSpace.Closeds.gc` `isClosed_iff` `Set.image_subset_iff` `CompleteSemilatticeInf.sInf_le` `hull_kernel_of_isClosed` `gc` `gc_closureOperator` `ClosureOperator.monotone`
`gc` 📖	mathematical	—	`GaloisConnection` `Set` `Set.Elem` `OrderDual` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `kernel` `hull` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `OrderDual.ofDual`	—	—
`gc_closureOperator` 📖	mathematical	—	`DFunLike.coe` `ClosureOperator` `Set` `Set.Elem` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `GaloisConnection.closureOperator` `OrderDual` `OrderDual.instPreorder` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `kernel` `hull` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `OrderDual.ofDual` `gc`	—	`gc` `Set.preimage_comp` `OrderDual.toDual_symm_eq` `Equiv.symm_comp_self` `Set.preimage_id_eq`
`hull_finsetInf` 📖	mathematical	`InfPrime`	`hull` `Finset.inf` `Set.preimage` `Set.Elem` `Set` `Set.instMembership` `SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `UpperSet.instSetLike` `upperClosure` `Finset` `Finset.instSetLike`	—	`coe_upperClosure` `Finset.cons_induction` `Set.iUnion_congr_Prop` `Finset.coe_empty` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.not_nonempty_iff_eq_empty` `Subtype.coe_prop` `isMax_iff_eq_top` `eq_top_iff` `Finset.inf_cons` `hull_inf` `Set.preimage_iUnion` `Finset.coe_cons` `Set.iUnion_iUnion_eq_or_left`
`hull_iSup` 📖	mathematical	—	`hull` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.iInter` `Set.Elem`	—	`Set.ext`
`hull_inf` 📖	mathematical	`InfPrime`	`hull` `SemilatticeInf.toMin` `Set` `Set.Elem` `Set.instUnion`	—	`Set.ext` `inf_le_of_left_le` `inf_le_of_right_le`
`hull_kernel_of_isClosed` 📖	mathematical	`InfPrime` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `OrderGenerates`	`hull` `kernel`	—	`isClosed_iff` `kernel_hull`
`hull_sSup` 📖	mathematical	—	`hull` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.sInter` `Set.Elem` `setOf` `Set` `Set.instMembership`	—	`Set.ext`
`isClosed_iff` 📖	mathematical	`InfPrime` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice`	`IsClosed` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `hull`	—	`isOpen_iff`
`isOpen_iff` 📖	mathematical	`InfPrime` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice`	`IsOpen` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Compl.compl` `Set.instCompl` `hull`	—	`TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'` `isTopologicalBasis_relativeLower` `Set.ext` `IsClosed.isOpen_compl` `isClosed_Ici` `Topology.IsLower.instClosedIciTopology`
`isTopologicalBasis_relativeLower` 📖	mathematical	`InfPrime`	`TopologicalSpace.IsTopologicalBasis` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `setOf` `Compl.compl` `Set.instCompl` `hull`	—	`Set.ext` `Function.Injective.preimage_image` `Subtype.val_injective` `upperClosure_singleton` `Set.image_val_compl` `Subtype.image_preimage_coe` `Set.diff_self_inter` `Subtype.coe_preimage_self` `Set.compl_eq_univ_diff` `CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `hull_finsetInf` `isTopologicalBasis_subtype` `Topology.IsLower.isTopologicalBasis`
`kernel_hull` 📖	mathematical	`OrderGenerates`	`kernel` `hull` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice`	—	`OrderDual.ofDual_toDual` `GaloisInsertion.l_u_eq`
`preimage_upperClosure_compl_finset` 📖	mathematical	`InfPrime`	`Set.preimage` `Set.Elem` `Set` `Set.instMembership` `Compl.compl` `Set.instCompl` `SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `UpperSet.instSetLike` `upperClosure` `Finset` `Finset.instSetLike` `hull` `Finset.inf`	—	`Set.preimage_compl` `hull_finsetInf`

---

← Back to Index