Documentation Verification Report

IsLocallyClosed

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

Statistics

Metric	Count
Definitions `IsLocallyClosed`	1
Theorems `isLocallyClosed_Icc`, `isLocallyClosed_Ici`, `isLocallyClosed_Ico`, `isLocallyClosed_Iic`, `isLocallyClosed_Iio`, `isLocallyClosed_Ioc`, `isLocallyClosed_Ioi`, `isLocallyClosed_Ioo`	8
Total	9

(root)

Definitions

Name	Category	Theorems
`IsLocallyClosed` 📖	MathDef	22 math math: `IsLocallyClosed.image`, `Topology.IsInducing.isLocallyClosed_iff`, `isLocallyClosed_Ioi`, `AlgebraicGeometry.isImmersion_eq_inf`, `isLocallyClosed_Ici`, `Topology.IsEmbedding.isLocallyClosed_iff`, `isLocallyClosed_Ico`, `AlgebraicGeometry.IsImmersion.isLocallyClosed_range`, `AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range`, `isLocallyClosed_Icc`, `IsLocallyClosed.inter`, `isLocallyClosed_Ioc`, `isLocallyClosed_Iio`, `IsOpen.isLocallyClosed`, `AlgebraicGeometry.isImmersion_iff`, `isLocallyClosed_tfae`, `IsLocallyClosed.preimage`, `isLocallyClosed_Ioo`, `IsClosed.isLocallyClosed`, `TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage`, `isLocallyClosed_Iic`, `isLocallyClosed_iff_isOpen_coborder`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocallyClosed_Icc` 📖	mathematical	—	`IsLocallyClosed` `Set.Icc`	—	`IsClosed.isLocallyClosed` `isClosed_Icc`
`isLocallyClosed_Ici` 📖	mathematical	—	`IsLocallyClosed` `Set.Ici`	—	`IsClosed.isLocallyClosed` `isClosed_Ici`
`isLocallyClosed_Ico` 📖	mathematical	—	`IsLocallyClosed` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.Iio_inter_Ici` `IsLocallyClosed.inter` `isLocallyClosed_Iio` `isLocallyClosed_Ici`
`isLocallyClosed_Iic` 📖	mathematical	—	`IsLocallyClosed` `Set.Iic`	—	`IsClosed.isLocallyClosed` `isClosed_Iic`
`isLocallyClosed_Iio` 📖	mathematical	—	`IsLocallyClosed` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.isLocallyClosed` `isOpen_Iio`
`isLocallyClosed_Ioc` 📖	mathematical	—	`IsLocallyClosed` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.Iic_inter_Ioi` `IsLocallyClosed.inter` `isLocallyClosed_Iic` `isLocallyClosed_Ioi`
`isLocallyClosed_Ioi` 📖	mathematical	—	`IsLocallyClosed` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.isLocallyClosed` `isOpen_Ioi`
`isLocallyClosed_Ioo` 📖	mathematical	—	`IsLocallyClosed` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsOpen.isLocallyClosed` `isOpen_Ioo`

---

← Back to Index