Sublocale

📁 Source: Mathlib/Order/Sublocale.lean

Statistics

Metric	Count
Definitions toSublocale, Sublocale, carrier, instCompleteLattice, instFrame, instHImp, instHeytingAlgebra, instInfSet, instOrderTop, instSemilatticeInf, giRestrict, instCoframe, instCoframeMinimalAxioms, instCompleteLattice, instPartialOrder, instSetLike, restrict, toNucleus, nucleusIsoSublocale	19
Theorems coe_toSublocale, mem_toSublocale, restrict_toSublocale, toSublocale_le_toSublocale, coe_himp, coe_iInf, coe_inf, coe_sInf, ext, ext_iff, himp_mem, himp_mem', iInf_mem, infClosed, inf_mem, mem_carrier, mem_mk, mk_le_mk, range_toNucleus, restrict_of_mem, sInf_mem, sInf_mem', toNucleus_apply, toNucleus_le_toNucleus, top_mem, eq_toSublocale, symm_eq_toNucleus	27
Total	46

Nucleus

Definitions

Name	Category	Theorems
toSublocale 📖	CompOp	5 math math: mem_toSublocale, coe_toSublocale, toSublocale_le_toSublocale, nucleusIsoSublocale.eq_toSublocale, restrict_toSublocale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toSublocale 📖	mathematical	—	SetLike.coe Sublocale Sublocale.instSetLike toSublocale Set.range DFunLike.coe Nucleus Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice instFunLike	—	—
mem_toSublocale 📖	mathematical	—	Sublocale SetLike.instMembership Sublocale.instSetLike toSublocale DFunLike.coe Nucleus Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice instFunLike	—	—
restrict_toSublocale 📖	mathematical	—	DFunLike.coe FrameHom Sublocale SetLike.instMembership Sublocale.instSetLike toSublocale Order.Frame.toCompleteLattice Sublocale.carrier.instCompleteLattice FrameHom.instFunLike Sublocale.restrict Nucleus Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instFunLike	—	sInf_image le_antisymm_iff iInf₂_le_of_le le_apply le_rfl idempotent monotone
toSublocale_le_toSublocale 📖	mathematical	—	Sublocale Preorder.toLE PartialOrder.toPreorder Sublocale.instPartialOrder toSublocale Nucleus Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice instPartialOrder	—	instIsConcreteLE

Sublocale

Definitions

Name	Category	Theorems
carrier 📖	CompOp	1 math math: mem_carrier
giRestrict 📖	CompOp	—
instCoframe 📖	CompOp	—
instCoframeMinimalAxioms 📖	CompOp	—
instCompleteLattice 📖	CompOp	—
instPartialOrder 📖	CompOp	5 math math: Nucleus.toSublocale_le_toSublocale, toNucleus_le_toNucleus, mk_le_mk, nucleusIsoSublocale.eq_toSublocale, nucleusIsoSublocale.symm_eq_toNucleus
instSetLike 📖	CompOp	14 math math: mem_carrier, coe_iInf, top_mem, Nucleus.mem_toSublocale, coe_inf, Nucleus.coe_toSublocale, mem_mk, coe_sInf, coe_himp, ext_iff, Nucleus.restrict_toSublocale, infClosed, range_toNucleus, toNucleus_apply
restrict 📖	CompOp	3 math math: Nucleus.restrict_toSublocale, restrict_of_mem, toNucleus_apply
toNucleus 📖	CompOp	4 math math: toNucleus_le_toNucleus, nucleusIsoSublocale.symm_eq_toNucleus, range_toNucleus, toNucleus_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_himp 📖	mathematical	—	Sublocale SetLike.instMembership instSetLike HImp.himp carrier.instHImp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra	—	—
coe_iInf 📖	mathematical	—	Sublocale SetLike.instMembership instSetLike iInf carrier.instInfSet ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice	—	—
coe_inf 📖	mathematical	—	Sublocale SetLike.instMembership instSetLike SemilatticeInf.toMin carrier.instSemilatticeInf Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice	—	—
coe_sInf 📖	mathematical	—	Sublocale SetLike.instMembership instSetLike InfSet.sInf carrier.instInfSet ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice Set.image	—	—
ext 📖	—	Sublocale SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	Sublocale SetLike.instMembership instSetLike	—	ext
himp_mem 📖	mathematical	Sublocale SetLike.instMembership instSetLike	HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra	—	himp_mem'
himp_mem' 📖	mathematical	Set Set.instMembership carrier	HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra	—	—
iInf_mem 📖	mathematical	Sublocale SetLike.instMembership instSetLike	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice	—	sInf_mem
infClosed 📖	mathematical	—	InfClosed Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice SetLike.coe Sublocale instSetLike	—	sInf_pair sInf_mem Set.pair_subset
inf_mem 📖	mathematical	Sublocale SetLike.instMembership instSetLike	SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice	—	infClosed
mem_carrier 📖	mathematical	—	Set Set.instMembership carrier Sublocale SetLike.instMembership instSetLike	—	—
mem_mk 📖	mathematical	Set Set.instMembership InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra	Sublocale SetLike.instMembership instSetLike	—	—
mk_le_mk 📖	mathematical	Set Set.instMembership InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra	Sublocale Preorder.toLE PartialOrder.toPreorder instPartialOrder Set.instHasSubset	—	—
range_toNucleus 📖	mathematical	—	Set.range DFunLike.coe Nucleus Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice Nucleus.instFunLike toNucleus SetLike.coe Sublocale instSetLike	—	Set.ext restrict_of_mem
restrict_of_mem 📖	mathematical	Sublocale SetLike.instMembership instSetLike	DFunLike.coe FrameHom Order.Frame.toCompleteLattice carrier.instCompleteLattice FrameHom.instFunLike restrict	—	GaloisInsertion.l_u_eq
sInf_mem 📖	mathematical	Set Set.instHasSubset SetLike.coe Sublocale instSetLike	SetLike.instMembership InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice	—	sInf_mem'
sInf_mem' 📖	mathematical	Set Set.instHasSubset carrier	Set.instMembership InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice	—	—
toNucleus_apply 📖	mathematical	—	DFunLike.coe Nucleus Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice Nucleus.instFunLike toNucleus Sublocale SetLike.instMembership instSetLike FrameHom carrier.instCompleteLattice FrameHom.instFunLike restrict	—	—
toNucleus_le_toNucleus 📖	mathematical	—	Nucleus Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice Preorder.toLE PartialOrder.toPreorder Nucleus.instPartialOrder toNucleus Sublocale instPartialOrder	—	range_toNucleus instIsConcreteLE
top_mem 📖	mathematical	—	Sublocale SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Order.Frame.toCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	sInf_empty sInf_mem Set.empty_subset

Sublocale.carrier

Definitions

Name	Category	Theorems
instCompleteLattice 📖	CompOp	3 math math: Nucleus.restrict_toSublocale, Sublocale.restrict_of_mem, Sublocale.toNucleus_apply
instFrame 📖	CompOp	—
instHImp 📖	CompOp	1 math math: Sublocale.coe_himp
instHeytingAlgebra 📖	CompOp	—
instInfSet 📖	CompOp	2 math math: Sublocale.coe_iInf, Sublocale.coe_sInf
instOrderTop 📖	CompOp	—
instSemilatticeInf 📖	CompOp	1 math math: Sublocale.coe_inf

(root)

Definitions

Name	Category	Theorems
Sublocale 📖	CompData	19 math math: Sublocale.mem_carrier, Sublocale.coe_iInf, Sublocale.top_mem, Nucleus.mem_toSublocale, Sublocale.coe_inf, Nucleus.coe_toSublocale, Nucleus.toSublocale_le_toSublocale, Sublocale.mem_mk, Sublocale.coe_sInf, Sublocale.coe_himp, Sublocale.ext_iff, Sublocale.toNucleus_le_toNucleus, Sublocale.mk_le_mk, nucleusIsoSublocale.eq_toSublocale, nucleusIsoSublocale.symm_eq_toNucleus, Nucleus.restrict_toSublocale, Sublocale.infClosed, Sublocale.range_toNucleus, Sublocale.toNucleus_apply
nucleusIsoSublocale 📖	CompOp	2 math math: nucleusIsoSublocale.eq_toSublocale, nucleusIsoSublocale.symm_eq_toNucleus

nucleusIsoSublocale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_toSublocale 📖	mathematical	—	Nucleus.toSublocale DFunLike.coe OrderIso OrderDual Nucleus Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice Sublocale OrderDual.instLE Preorder.toLE PartialOrder.toPreorder Nucleus.instPartialOrder Sublocale.instPartialOrder instFunLikeOrderIso nucleusIsoSublocale	—	—
symm_eq_toNucleus 📖	mathematical	—	Sublocale.toNucleus DFunLike.coe OrderIso Sublocale OrderDual Nucleus Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Order.Frame.toCompleteLattice Preorder.toLE PartialOrder.toPreorder Sublocale.instPartialOrder OrderDual.instLE Nucleus.instPartialOrder instFunLikeOrderIso OrderIso.symm nucleusIsoSublocale	—	—

---

← Back to Index