NhdsSet

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

Statistics

Metric	Count
Definitions	0
Theorems Icc_mem_nhdsSet_Icc, Icc_mem_nhdsSet_Ico, Icc_mem_nhdsSet_Ioc, Ici_mem_nhdsSet_Icc, Ici_mem_nhdsSet_Ici, Ici_mem_nhdsSet_Ici_iff, Ici_mem_nhdsSet_Ico, Ici_mem_nhdsSet_Ioc, Ico_mem_nhdsSet_Icc, Ico_mem_nhdsSet_Ico, Ico_mem_nhdsSet_Ioc, Iic_mem_nhdsSet_Icc, Iic_mem_nhdsSet_Ico, Iic_mem_nhdsSet_Iic, Iic_mem_nhdsSet_Iic_iff, Iic_mem_nhdsSet_Ioc, Iio_mem_nhdsSet_Icc, Iio_mem_nhdsSet_Ico, Iio_mem_nhdsSet_Iic, Iio_mem_nhdsSet_Iic_iff, Iio_mem_nhdsSet_Ioc, Ioc_mem_nhdsSet_Icc, Ioc_mem_nhdsSet_Ico, Ioc_mem_nhdsSet_Ioc, Ioi_mem_nhdsSet_Icc, Ioi_mem_nhdsSet_Ici, Ioi_mem_nhdsSet_Ici_iff, Ioi_mem_nhdsSet_Ico, Ioi_mem_nhdsSet_Ioc, Ioo_mem_nhdsSet_Icc, Ioo_mem_nhdsSet_Ico, Ioo_mem_nhdsSet_Ioc, hasBasis_nhdsSet_Ici_Ici, hasBasis_nhdsSet_Ici_Ioi, hasBasis_nhdsSet_Iic_Iic, hasBasis_nhdsSet_Iic_Iio, nhdsSet_Icc, nhdsSet_Ici, nhdsSet_Ico, nhdsSet_Iic, nhdsSet_Iio, nhdsSet_Ioc, nhdsSet_Ioi, nhdsSet_Ioo	44
Total	44

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_mem_nhdsSet_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Icc	—	Filter.inter_mem Ici_mem_nhdsSet_Icc Iic_mem_nhdsSet_Icc
Icc_mem_nhdsSet_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	Set Filter Filter.instMembership nhdsSet Set.Ico Set.Icc	—	Filter.inter_mem Ici_mem_nhdsSet_Ico Iic_mem_nhdsSet_Ico
Icc_mem_nhdsSet_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhdsSet Set.Ioc Set.Icc	—	Filter.inter_mem Ici_mem_nhdsSet_Ioc Iic_mem_nhdsSet_Ioc
Ici_mem_nhdsSet_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Icc Set.Ici	—	Filter.mem_of_superset Ioi_mem_nhdsSet_Icc Set.Ioi_subset_Ici_self
Ici_mem_nhdsSet_Ici 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ici	—	Filter.mem_of_superset Ioi_mem_nhdsSet_Ici Set.Ioi_subset_Ici_self
Ici_mem_nhdsSet_Ici_iff 📖	mathematical	—	Set Filter Filter.instMembership nhdsSet Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	Iic_mem_nhdsSet_Iic_iff instOrderTopologyOrderDual
Ici_mem_nhdsSet_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ico Set.Ici	—	nhdsSet_mono Set.Ico_subset_Icc_self Ici_mem_nhdsSet_Icc
Ici_mem_nhdsSet_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ioc Set.Ici	—	Filter.mem_of_superset Ioi_mem_nhdsSet_Ioc Set.Ioi_subset_Ici_self
Ico_mem_nhdsSet_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Icc Set.Ico	—	Filter.inter_mem Ici_mem_nhdsSet_Icc Iio_mem_nhdsSet_Icc
Ico_mem_nhdsSet_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	Set Filter Filter.instMembership nhdsSet Set.Ico	—	Filter.inter_mem Ici_mem_nhdsSet_Ico Iio_mem_nhdsSet_Ico
Ico_mem_nhdsSet_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhdsSet Set.Ioc Set.Ico	—	Filter.inter_mem Ici_mem_nhdsSet_Ioc Iio_mem_nhdsSet_Ioc
Iic_mem_nhdsSet_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Icc Set.Iic	—	Filter.mem_of_superset Iio_mem_nhdsSet_Icc Set.Iio_subset_Iic_self
Iic_mem_nhdsSet_Ico 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ico Set.Iic	—	Filter.mem_of_superset Iio_mem_nhdsSet_Ico Set.Iio_subset_Iic_self
Iic_mem_nhdsSet_Iic 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Iic	—	Ici_mem_nhdsSet_Ici instOrderClosedTopologyOrderDual
Iic_mem_nhdsSet_Iic_iff 📖	mathematical	—	Set Filter Filter.instMembership nhdsSet Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	Filter.HasBasis.mem_iff hasBasis_nhdsSet_Iic_Iic LT.lt.trans_le Set.Iic_subset_Iic Set.Subset.rfl
Iic_mem_nhdsSet_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ioc Set.Iic	—	nhdsSet_mono Set.Ioc_subset_Icc_self Iic_mem_nhdsSet_Icc
Iio_mem_nhdsSet_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Icc Set.Iio	—	nhdsSet_mono Set.Icc_subset_Iic_self Iio_mem_nhdsSet_Iic
Iio_mem_nhdsSet_Ico 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ico Set.Iio	—	nhdsSet_mono Set.Ico_subset_Iio_self nhdsSet_Iio
Iio_mem_nhdsSet_Iic 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Iic Set.Iio	—	Iio_mem_nhdsSet_Iic_iff
Iio_mem_nhdsSet_Iic_iff 📖	mathematical	—	Set Filter Filter.instMembership nhdsSet Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iio Preorder.toLT	—	Ioi_mem_nhdsSet_Ici_iff instOrderClosedTopologyOrderDual
Iio_mem_nhdsSet_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ioc Set.Iio	—	nhdsSet_mono Set.Ioc_subset_Icc_self Iio_mem_nhdsSet_Icc
Ioc_mem_nhdsSet_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Icc Set.Ioc	—	Filter.inter_mem Ioi_mem_nhdsSet_Icc Iic_mem_nhdsSet_Icc
Ioc_mem_nhdsSet_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	Set Filter Filter.instMembership nhdsSet Set.Ico Set.Ioc	—	Filter.inter_mem Ioi_mem_nhdsSet_Ico Iic_mem_nhdsSet_Ico
Ioc_mem_nhdsSet_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhdsSet Set.Ioc	—	Filter.inter_mem Ioi_mem_nhdsSet_Ioc Iic_mem_nhdsSet_Ioc
Ioi_mem_nhdsSet_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Icc Set.Ioi	—	nhdsSet_mono Set.Icc_subset_Ici_self Ioi_mem_nhdsSet_Ici
Ioi_mem_nhdsSet_Ici 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ici Set.Ioi	—	Ioi_mem_nhdsSet_Ici_iff
Ioi_mem_nhdsSet_Ici_iff 📖	mathematical	—	Set Filter Filter.instMembership nhdsSet Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioi Preorder.toLT	—	IsOpen.mem_nhdsSet isOpen_Ioi instClosedIicTopology Set.Ici_subset_Ioi
Ioi_mem_nhdsSet_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ico Set.Ioi	—	nhdsSet_mono Set.Ico_subset_Icc_self Ioi_mem_nhdsSet_Icc
Ioi_mem_nhdsSet_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Ioc Set.Ioi	—	nhdsSet_mono Set.Ioc_subset_Ioi_self nhdsSet_Ioi
Ioo_mem_nhdsSet_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsSet Set.Icc Set.Ioo	—	Filter.inter_mem Ioi_mem_nhdsSet_Icc Iio_mem_nhdsSet_Icc
Ioo_mem_nhdsSet_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	Set Filter Filter.instMembership nhdsSet Set.Ico Set.Ioo	—	Filter.inter_mem Ioi_mem_nhdsSet_Ico Iio_mem_nhdsSet_Ico
Ioo_mem_nhdsSet_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhdsSet Set.Ioc Set.Ioo	—	Filter.inter_mem Ioi_mem_nhdsSet_Ioc Iio_mem_nhdsSet_Ioc
hasBasis_nhdsSet_Ici_Ici 📖	mathematical	—	Filter.HasBasis nhdsSet Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	hasBasis_nhdsSet_Iic_Iic instOrderTopologyOrderDual
hasBasis_nhdsSet_Ici_Ioi 📖	mathematical	—	Filter.HasBasis nhdsSet Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioi	—	hasBasis_nhdsSet_Iic_Iio instOrderTopologyOrderDual
hasBasis_nhdsSet_Iic_Iic 📖	mathematical	—	Filter.HasBasis nhdsSet Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	Set.Nonempty.to_subtype Filter.nonempty_of_mem self_mem_nhdsWithin Filter.HasBasis.to_hasBasis hasBasis_nhdsSet_Iic_Iio Ioo_mem_nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology Set.Iio_subset_Iic_self
hasBasis_nhdsSet_Iic_Iio 📖	mathematical	—	Filter.HasBasis nhdsSet Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Iio	—	exists_Ico_subset_of_mem_nhds Filter.mem_principal Filter.mem_sup nhdsSet_Iic OrderTopology.to_orderClosedTopology Set.nonempty_coe_sort HasSubset.Subset.trans Set.instIsTransSubset Set.Iio_subset_Iio_union_Ico Set.union_subset Filter.mem_of_superset Iio_mem_nhdsSet_Iic
nhdsSet_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	nhdsSet Set.Icc Filter Filter.instSup nhds Filter.principal Set.Ioo	—	LE.le.eq_or_lt Set.Icc_self nhdsSet_singleton sup_of_le_left Set.Ioo_eq_empty Filter.principal_empty Set.Ioc_insert_left nhdsSet_insert nhdsSet_Ioc sup_assoc
nhdsSet_Ici 📖	mathematical	—	nhdsSet Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instSup nhds Filter.principal Set.Ioi	—	Set.Ioi_insert nhdsSet_insert nhdsSet_Ioi
nhdsSet_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	nhdsSet Set.Ico Filter Filter.instSup nhds Filter.principal Set.Ioo	—	Set.Ioo_insert_left nhdsSet_insert nhdsSet_Ioo
nhdsSet_Iic 📖	mathematical	—	nhdsSet Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instSup nhds Filter.principal Set.Iio	—	nhdsSet_Ici instOrderClosedTopologyOrderDual
nhdsSet_Iio 📖	mathematical	—	nhdsSet Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.principal	—	IsOpen.nhdsSet_eq isOpen_Iio instClosedIciTopology
nhdsSet_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	nhdsSet Set.Ioc Filter Filter.instSup nhds Filter.principal Set.Ioo	—	Set.Ioo_insert_right nhdsSet_insert nhdsSet_Ioo
nhdsSet_Ioi 📖	mathematical	—	nhdsSet Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.principal	—	IsOpen.nhdsSet_eq isOpen_Ioi instClosedIicTopology
nhdsSet_Ioo 📖	mathematical	—	nhdsSet Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.principal	—	IsOpen.nhdsSet_eq isOpen_Ioo

---

← Back to Index