Documentation Verification Report

ProjIcc

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

Statistics

Metric	Count
Definitions	0
Theorems `IccExtend`, `Icc_extend'`, `IccExtend`, `IccExtend`, `continuous_IccExtend_iff`, `continuous_projIcc`, `isQuotientMap_projIcc`	7
Total	7

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IccExtend` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Continuous` `Set.Elem` `Set.Icc` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase`	`Set.IccExtend`	—	`comp` `prodMk` `continuous_id` `continuous_projIcc`
`Icc_extend'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Continuous` `Set.Elem` `Set.Icc` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	`Set.IccExtend`	—	`comp` `continuous_projIcc`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IccExtend` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ContinuousAt` `Set.Elem` `Set.Icc` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `Set.projIcc`	`Set.IccExtend`	—	`comp` `prodMk` `continuousAt_id` `Continuous.continuousAt` `continuous_projIcc`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IccExtend` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.Tendsto` `Set.Elem` `Set.Icc` `Function.HasUncurry.uncurry` `Function.hasUncurryInduction` `Function.hasUncurryBase` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.map` `Set.projIcc`	`Set.IccExtend`	—	`comp` `prodMap` `Filter.tendsto_id` `Filter.tendsto_map`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_IccExtend_iff` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Continuous` `Set.IccExtend` `Set.Elem` `Set.Icc` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Topology.IsQuotientMap.continuous_iff` `isQuotientMap_projIcc`
`continuous_projIcc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Continuous` `Set.Elem` `Set.Icc` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.projIcc`	—	`Continuous.max` `OrderTopology.to_orderClosedTopology` `continuous_const` `Continuous.min` `continuous_id'`
`isQuotientMap_projIcc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Topology.IsQuotientMap` `Set.Elem` `Set.Icc` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.projIcc`	—	`Topology.isQuotientMap_iff` `Set.projIcc_surjective` `IsOpen.preimage` `continuous_projIcc` `Set.ext` `Set.projIcc_val`

---

← Back to Index