FrameAdjunction

📁 Source: Mathlib/Topology/Order/Category/FrameAdjunction.lean

Statistics

Metric	Count
Definitions PT, instTopologicalSpace, adjunctionTopToLocalePT, counitAppCont, localePointOfSpacePoint, openOfElementHom, pt	7
Theorems isOpen_iff, localePointOfSpacePoint_toFun, openOfElementHom_toFun	3
Total	10

Locale

Definitions

Name	Category	Theorems
PT 📖	CompOp	2 math math: PT.isOpen_iff, openOfElementHom_toFun
adjunctionTopToLocalePT 📖	CompOp	—
counitAppCont 📖	CompOp	—
localePointOfSpacePoint 📖	CompOp	1 math math: localePointOfSpacePoint_toFun
openOfElementHom 📖	CompOp	1 math math: openOfElementHom_toFun
pt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
localePointOfSpacePoint_toFun 📖	mathematical	—	DFunLike.coe FrameHom TopologicalSpace.Opens TopologicalSpace.Opens.instCompleteLattice Prop.instCompleteLattice FrameHom.instFunLike localePointOfSpacePoint SetLike.instMembership TopologicalSpace.Opens.instSetLike	—	—
openOfElementHom_toFun 📖	mathematical	—	DFunLike.coe FrameHom Set PT CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra FrameHom.instFunLike openOfElementHom setOf Prop.instCompleteLattice	—	—

Locale.PT

Definitions

Name	Category	Theorems
instTopologicalSpace 📖	CompOp	1 math math: isOpen_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_iff 📖	mathematical	—	IsOpen Locale.PT instTopologicalSpace setOf DFunLike.coe FrameHom.instFunLike Prop.instCompleteLattice	—	—

---

← Back to Index