IsLUB

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

Statistics

Metric	Count
Definitions IsLUB	1
Theorems isCompact_Icc, ciInf, ciInf', ciSup, ciSup', exists_seq_strictAnti_tendsto, exists_seq_strictAnti_tendsto_of_lt, exists_seq_strictMono_tendsto, exists_seq_strictMono_tendsto_of_lt, isGLB_inter_iff, isLUB_inter_iff, lowerBounds_image, upperBounds_image, exists_seq_strictAnti_tendsto, exists_seq_strictAnti_tendsto_of_lt, exists_seq_strictMono_tendsto, exists_seq_strictMono_tendsto_of_lt, isGLB_mem, isLUB_mem, lowerClosure, upperClosure, exists_seq_antitone_tendsto, exists_seq_strictAnti_tendsto_of_notMem, frequently_mem, frequently_nhds_mem, isGLB_of_tendsto, isLUB_of_tendsto, mem_closure, mem_lowerBounds_of_tendsto, mem_of_isClosed, mem_upperBounds_of_tendsto, nhdsWithin_neBot, exists_seq_monotone_tendsto, exists_seq_strictMono_tendsto_of_notMem, frequently_mem, frequently_nhds_mem, isGLB_of_tendsto, isLUB_of_tendsto, mem_closure, mem_lowerBounds_of_tendsto, mem_of_isClosed, mem_upperBounds_of_tendsto, nhdsWithin_neBot, exists_seq_strictAnti_strictMono_tendsto, exists_seq_strictAnti_tendsto, exists_seq_strictAnti_tendsto', exists_seq_strictAnti_tendsto_nhdsWithin, exists_seq_strictMono_tendsto, exists_seq_strictMono_tendsto', exists_seq_strictMono_tendsto_nhdsWithin, exists_seq_tendsto_sInf, exists_seq_tendsto_sSup, isGLB_iff_of_subset_of_subset_closure, isGLB_of_mem_closure, isGLB_of_mem_nhds, isLUB_iff_of_subset_of_subset_closure, isLUB_of_mem_closure, isLUB_of_mem_nhds, lowerClosure_eq_Iic_csSup, upperClosure_eq_Ici_csInf	60
Total	61

ConditionallyCompleteLinearOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_Icc 📖	mathematical	—	IsCompact Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder toConditionallyCompleteLattice	—	le_or_gt Mathlib.Tactic.Push.not_and_eq le_trans pure_le_nhds instReflLe Set.Icc_self isLUB_csSup IsLUB.exists_between Filter.mp_mem Ultrafilter.compl_mem_iff_notMem Filter.univ_mem' nhds_eq_order iInf_congr_Prop Filter.mem_of_superset le_of_not_gt notMem_of_csSup_lt Set.Icc_eq_empty Ultrafilter.neBot supSet_to_nonempty

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ciInf 📖	mathematical	Dense Continuous BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instMembership	—	ciSup instClosedIicTopologyOrderDual
ciInf' 📖	mathematical	Dense Continuous	iInf Set.Elem ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership	—	ciSup' instClosedIicTopologyOrderDual
ciSup 📖	mathematical	Dense Continuous BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instMembership	—	sSup_range isEmpty_or_nonempty Set.range_eq_empty instIsEmptySubtype IsLUB.unique isLUB_csSup Set.range_nonempty isLUB_congr upperBounds_image isLUB_ciSup_set BddAbove.mono nonempty
ciSup' 📖	mathematical	Dense Continuous	iSup Set.Elem ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership	—	ciSup BddAbove.mono Set.range_comp Subtype.range_coe_subtype Continuous.range_subset_closure_image_dense BddAbove.closure Mathlib.Tactic.Contrapose.contrapose₄ ciSup_of_not_bddAbove
exists_seq_strictAnti_tendsto 📖	mathematical	Dense	StrictAnti Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.instInter Set.Ioi Filter.Tendsto Filter.atTop nhds	—	exists_seq_strictMono_tendsto instOrderTopologyOrderDual OrderDual.denselyOrdered OrderDual.noMinOrder instFirstCountableTopologyOrderDual
exists_seq_strictAnti_tendsto_of_lt 📖	mathematical	Dense Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	StrictAnti Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.instInter Set.Ioo Filter.Tendsto Filter.atTop nhds	—	Set.Ioo_toDual exists_seq_strictMono_tendsto_of_lt instOrderTopologyOrderDual OrderDual.denselyOrdered instFirstCountableTopologyOrderDual OrderDual.toDual_lt_toDual
exists_seq_strictMono_tendsto 📖	mathematical	Dense	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.instInter Set.Iio Filter.Tendsto Filter.atTop nhds	—	NoMinOrder.exists_lt exists_seq_strictMono_tendsto_of_lt
exists_seq_strictMono_tendsto_of_lt 📖	mathematical	Dense Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.instInter Set.Ioo Filter.Tendsto Filter.atTop nhds	—	exists_between OrderTopology.to_orderClosedTopology Set.mem_inter isLUB_inter_iff instClosedIicTopology isOpen_Ioo isLUB_Ioo IsLUB.exists_seq_strictMono_tendsto_of_notMem FirstCountableTopology.nhds_generated_countable
isGLB_inter_iff 📖	mathematical	Dense IsOpen	IsGLB Preorder.toLE Set Set.instInter	—	isLUB_inter_iff instClosedIicTopologyOrderDual
isLUB_inter_iff 📖	mathematical	Dense IsOpen	IsLUB Preorder.toLE Set Set.instInter	—	isLUB_iff_of_subset_of_subset_closure open_subset_closure_inter
lowerBounds_image 📖	mathematical	Dense Continuous	lowerBounds Preorder.toLE Set.image Set.range	—	upperBounds_image instClosedIicTopologyOrderDual
upperBounds_image 📖	mathematical	Dense Continuous	upperBounds Preorder.toLE Set.image Set.range	—	subset_antisymm Set.instAntisymmSubset subset_trans Set.instIsTransSubset Filter.Frequently.mem_of_closed Filter.Frequently.mono mem_closure_iff_frequently isClosed_Iic upperBounds_mono Continuous.range_subset_closure_image_dense le_rfl Set.image_subset_range

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_seq_strictAnti_tendsto 📖	mathematical	DenseRange Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	StrictAnti Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Ioi Filter.Tendsto Filter.atTop nhds	—	exists_seq_strictMono_tendsto instOrderTopologyOrderDual OrderDual.denselyOrdered OrderDual.noMinOrder instFirstCountableTopologyOrderDual Monotone.dual
exists_seq_strictAnti_tendsto_of_lt 📖	mathematical	DenseRange Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	StrictAnti Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Ioo Filter.Tendsto Filter.atTop nhds	—	Set.Ioo_toDual exists_seq_strictMono_tendsto_of_lt instOrderTopologyOrderDual OrderDual.denselyOrdered instFirstCountableTopologyOrderDual Monotone.dual OrderDual.toDual_lt_toDual
exists_seq_strictMono_tendsto 📖	mathematical	DenseRange Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Iio Filter.Tendsto Filter.atTop nhds	—	Dense.exists_seq_strictMono_tendsto Monotone.reflect_lt
exists_seq_strictMono_tendsto_of_lt 📖	mathematical	DenseRange Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Ioo Filter.Tendsto Filter.atTop nhds	—	Dense.exists_seq_strictMono_tendsto_of_lt Monotone.reflect_lt

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGLB_mem 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Set Set.instMembership	—	IsGLB.mem_of_isClosed
isLUB_mem 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Set Set.instMembership	—	IsLUB.mem_of_isClosed
lowerClosure 📖	mathematical	—	IsClosed LowerSet.carrier Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice lowerClosure	—	upperClosure instOrderTopologyOrderDual
upperClosure 📖	mathematical	—	IsClosed SetLike.coe UpperSet Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice UpperSet.instSetLike upperClosure	—	Set.eq_empty_or_nonempty upperClosure_empty T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology isClosed_Ici instClosedIciTopology upperClosure_eq_Ici_csInf isClosed_univ upperClosure_eq_bot

IsGLB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_seq_antitone_tendsto 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Antitone Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE Filter.Tendsto Filter.atTop nhds Set Set.instMembership	—	IsLUB.exists_seq_monotone_tendsto instOrderTopologyOrderDual
exists_seq_strictAnti_tendsto_of_notMem 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Nonempty	StrictAnti Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Filter.Tendsto Filter.atTop nhds Set Set.instMembership	—	IsLUB.exists_seq_strictMono_tendsto_of_notMem instOrderTopologyOrderDual
frequently_mem 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Filter.Frequently Set Set.instMembership nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	IsLUB.frequently_mem instOrderTopologyOrderDual
frequently_nhds_mem 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Filter.Frequently Set Set.instMembership nhds	—	Filter.Frequently.filter_mono frequently_mem inf_le_left
isGLB_of_tendsto 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsGLB Preorder.toLE Set.Nonempty Filter.Tendsto nhdsWithin nhds	IsGLB Preorder.toLE Set.image	—	IsLUB.isLUB_of_tendsto instOrderTopologyOrderDual instOrderClosedTopologyOrderDual MonotoneOn.dual
isLUB_of_tendsto 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsGLB Preorder.toLE Set.Nonempty Filter.Tendsto nhdsWithin nhds	IsLUB Preorder.toLE Set.image	—	isGLB_of_tendsto instOrderClosedTopologyOrderDual
mem_closure 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Set Set.instMembership closure	—	Filter.Frequently.mem_closure frequently_nhds_mem
mem_lowerBounds_of_tendsto 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsGLB Preorder.toLE Filter.Tendsto nhdsWithin nhds	Set Set.instMembership lowerBounds Preorder.toLE Set.image	—	IsLUB.mem_upperBounds_of_tendsto instOrderTopologyOrderDual instOrderClosedTopologyOrderDual MonotoneOn.dual
mem_of_isClosed 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Set Set.instMembership	—	IsClosed.closure_subset mem_closure
mem_upperBounds_of_tendsto 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsGLB Preorder.toLE Filter.Tendsto nhdsWithin nhds	Set Set.instMembership upperBounds Preorder.toLE Set.image	—	mem_lowerBounds_of_tendsto instOrderClosedTopologyOrderDual
nhdsWithin_neBot 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Filter.NeBot nhdsWithin	—	IsLUB.nhdsWithin_neBot instOrderTopologyOrderDual

IsLUB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_seq_monotone_tendsto 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Monotone Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE Filter.Tendsto Filter.atTop nhds Set Set.instMembership	—	monotone_const le_rfl tendsto_const_nhds exists_seq_strictMono_tendsto_of_notMem StrictMono.monotone LT.lt.le
exists_seq_strictMono_tendsto_of_notMem 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Nonempty	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Filter.Tendsto Filter.atTop nhds Set Set.instMembership	—	Filter.exists_seq_forall_of_frequently TopologicalSpace.isCountablyGenerated_nhdsWithin frequently_mem Filter.Tendsto.mono_right nhdsWithin_le_nhds LE.le.lt_of_ne Filter.Tendsto.eventually lt_mem_nhds strictMono_nat_of_lt_succ Function.iterate_succ_apply' Filter.Tendsto.comp StrictMono.tendsto_atTop Filter.Eventually.exists Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.Eventually.and Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder
frequently_mem 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Filter.Frequently Set Set.instMembership nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	LE.le.eq_or_lt Filter.Eventually.self_of_nhdsWithin le_rfl mem_nhdsLE_iff_exists_Ioc_subset' exists_between
frequently_nhds_mem 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Filter.Frequently Set Set.instMembership nhds	—	Filter.Frequently.filter_mono frequently_mem inf_le_left
isGLB_of_tendsto 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsLUB Preorder.toLE Set.Nonempty Filter.Tendsto nhdsWithin nhds	IsGLB Preorder.toLE Set.image	—	isLUB_of_tendsto instOrderClosedTopologyOrderDual
isLUB_of_tendsto 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsLUB Preorder.toLE Set.Nonempty Filter.Tendsto nhdsWithin nhds	IsLUB Preorder.toLE Set.image	—	mem_upperBounds_of_tendsto le_of_tendsto instClosedIicTopology nhdsWithin_neBot Filter.mem_of_superset self_mem_nhdsWithin Set.mem_image_of_mem
mem_closure 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Set Set.instMembership closure	—	Filter.Frequently.mem_closure frequently_nhds_mem
mem_lowerBounds_of_tendsto 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsLUB Preorder.toLE Filter.Tendsto nhdsWithin nhds	Set Set.instMembership lowerBounds Preorder.toLE Set.image	—	mem_upperBounds_of_tendsto instOrderClosedTopologyOrderDual
mem_of_isClosed 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Set Set.instMembership	—	IsClosed.closure_subset mem_closure
mem_upperBounds_of_tendsto 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsLUB Preorder.toLE Filter.Tendsto nhdsWithin nhds	Set Set.instMembership upperBounds Preorder.toLE Set.image	—	inter_Ici_of_mem ge_of_tendsto instClosedIciTopology nhdsWithin_neBot le_rfl Filter.Tendsto.mono_left nhdsWithin_mono Set.inter_subset_left Filter.mem_of_superset self_mem_nhdsWithin
nhdsWithin_neBot 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	Filter.NeBot nhdsWithin	—	mem_closure_iff_nhdsWithin_neBot mem_closure

(root)

Definitions

Name	Category	Theorems
IsLUB 📖	MathDef	118 math math: IsLUB.union, OrderIso.isLUB_image, isLUB_lowerBounds, lp.isLUB_norm, isLUB_singleton, IsLUB.range_of_tendsto, isLUB_of_tendsto_atBot, isLUB_iff_sSup_eq, isLUB_image2_of_isGLB_isGLB, IsLUB.mul_left, Preorder.hasColimit_iff_hasLUB, GaloisConnection.isLUB_l_image, isLUB_iff_le_iff, isGLB_inv', OrderIso.isLUB_image', IsGLB.neg, exists_lub_Iio, isLUB_iSup, Order.IsNormal.isLUB_image_Iio_of_isSuccLimit, isAtomistic_iff, DirectedOn.isLUB_sSup, IsLUB.sub, isLUB_ciSup, isLUB_hasProd, Finset.isLUB_sup_id, isLUB_iff_of_subset_of_subset_closure, isLUB_pair, IsCompact.isLUB_sSup, isLUB_inv, IsLUB.prod, Order.IsSuccPrelimit.isLUB_Iio, isLUB_neg', isLUB_congr, IsCompact.exists_isLUB, CompleteSemilatticeSup.isLUB_sSup, IsAtomistic.isLUB_atoms, Real.isLUB_of_tendsto_monotone_bddAbove, isLUB_hasProd', isGLB_inv, isLUB_Iio, isGLB_neg, GaloisConnection.isLUB_u, IsLUB.mul, isGLB_upperBounds, isLUB_Ioo, IsMaxOn.isLUB, GaloisInsertion.isLUB_of_u_image, isLUB_univ, DirectedOn.isLUB_ciSup_set, isLUB_inv', IsGLB.dual, IsLUB.insert, IsLUB.of_subset_of_superset, isLUB_atoms_top, isLUB_Ioc, Order.IsSuccLimit.isLUB_Iio, isLUB_iUnion_iff_of_isLUB, isLUB_of_mem_nhds, Order.isLUB_Iio_iff_isSuccPrelimit, Order.IsNormal.map_isLUB, isLUB_neg, isLUB_prod, Finset.isLUB_sup', IsGreatest.isLUB, Finset.isLUB_sup, IsLUB.of_image, IsLUB.mul_right, OrderIso.isLUB_preimage, CompletePartialOrder.scottContinuous, Preorder.isLUB_of_isColimit, isLUB_hasSum', OmegaCompletePartialOrder.ωScottContinuous.isLUB, CompleteLattice.isLUB_sSup, isLUB_ciSup_set, isLUB_Ico, isGLB_neg', GaloisCoinsertion.isLUB_of_l_image, ConditionallyCompletePartialOrderSup.isLUB_csSup_of_directed, Scott.isωSup_iff_isLUB, IsLUB.add, IsGLB.isLUB_of_tendsto, WithTop.isLUB_sSup, isLUB_Icc, Real.sSup_def, isLUB_empty_iff, isLUB_sSup, Filter.isLUB_sSup, IsLUB.isLUB_of_tendsto, CompletePartialOrder.lubOfDirected, isLUB_of_tendsto_atTop, isLUB_csSup, exists_countable_lowerSemicontinuous_isLUB, isLUB_biSup, isLUB_image2_of_isLUB_isGLB, isLUB_empty, OrderIso.isLUB_preimage', isLUB_hasSum, Real.isLUB_sSup, Dense.isLUB_inter_iff, isLUB_image2_of_isGLB_isLUB, Real.exists_isLUB, isLUB_supClosure, isLUB_pi, isLUB_atoms_le, Real.isLUB_of_tendsto_monotoneOn_bddAbove_nat_Ici, DirectedOn.isLUB_csSup, isLUB_csSup', IsLUB.inter_Ici_of_mem, ConditionallyCompleteLattice.isLUB_csSup, isLUB_Iic, WithTop.isLUB_sSup', IsLUB.div, IsGLB.inv, isLUB_of_mem_closure, isLUB_image2_of_isLUB_isLUB, OmegaCompletePartialOrder.isLUB_range_ωSup, Finset.isLUB_iff_isGreatest, Directed.isLUB_ciSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_seq_strictAnti_strictMono_tendsto 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	StrictAnti Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder StrictMono Set Set.instMembership Set.Ioo Preorder.toLT Filter.Tendsto Filter.atTop nhds	—	exists_seq_strictAnti_tendsto' exists_seq_strictMono_tendsto' LT.lt.trans LE.le.trans_lt StrictAnti.antitone zero_le Nat.instCanonicallyOrderedAdd
exists_seq_strictAnti_tendsto 📖	mathematical	—	StrictAnti Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Filter.Tendsto Filter.atTop nhds	—	exists_seq_strictMono_tendsto instOrderTopologyOrderDual OrderDual.denselyOrdered OrderDual.noMinOrder instFirstCountableTopologyOrderDual
exists_seq_strictAnti_tendsto' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	StrictAnti Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Ioo Filter.Tendsto Filter.atTop nhds	—	Set.Ioo_toDual exists_seq_strictMono_tendsto' OrderDual.denselyOrdered instOrderTopologyOrderDual instFirstCountableTopologyOrderDual OrderDual.toDual_lt_toDual
exists_seq_strictAnti_tendsto_nhdsWithin 📖	mathematical	—	StrictAnti Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Filter.Tendsto Filter.atTop nhdsWithin Set.Ioi	—	exists_seq_strictMono_tendsto_nhdsWithin instOrderTopologyOrderDual OrderDual.denselyOrdered OrderDual.noMinOrder instFirstCountableTopologyOrderDual
exists_seq_strictMono_tendsto 📖	mathematical	—	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Filter.Tendsto Filter.atTop nhds	—	NoMinOrder.exists_lt exists_seq_strictMono_tendsto'
exists_seq_strictMono_tendsto' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Ioo Filter.Tendsto Filter.atTop nhds	—	lt_irrefl Set.nonempty_Ioo IsLUB.exists_seq_strictMono_tendsto_of_notMem FirstCountableTopology.nhds_generated_countable isLUB_Ioo
exists_seq_strictMono_tendsto_nhdsWithin 📖	mathematical	—	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Filter.Tendsto Filter.atTop nhdsWithin Set.Iio	—	exists_seq_strictMono_tendsto tendsto_nhdsWithin_mono_right Set.range_subset_iff tendsto_nhdsWithin_range
exists_seq_tendsto_sInf 📖	mathematical	Set.Nonempty BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Antitone Nat.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.Tendsto Filter.atTop nhds InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instMembership	—	exists_seq_tendsto_sSup instOrderTopologyOrderDual instFirstCountableTopologyOrderDual
exists_seq_tendsto_sSup 📖	mathematical	Set.Nonempty BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Monotone Nat.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.Tendsto Filter.atTop nhds SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership	—	IsLUB.exists_seq_monotone_tendsto FirstCountableTopology.nhds_generated_countable isLUB_csSup
isGLB_iff_of_subset_of_subset_closure 📖	mathematical	Set Set.instHasSubset closure	IsGLB Preorder.toLE	—	isLUB_iff_of_subset_of_subset_closure instClosedIicTopologyOrderDual
isGLB_of_mem_closure 📖	mathematical	Set Set.instMembership lowerBounds Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder closure	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isLUB_of_mem_closure instOrderTopologyOrderDual
isGLB_of_mem_nhds 📖	mathematical	Set Set.instMembership lowerBounds Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instMembership	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isLUB_of_mem_nhds instOrderTopologyOrderDual
isLUB_iff_of_subset_of_subset_closure 📖	mathematical	Set Set.instHasSubset closure	IsLUB Preorder.toLE	—	isLUB_congr HasSubset.Subset.antisymm Set.instAntisymmSubset upperBounds_mono_set upperBounds_closure
isLUB_of_mem_closure 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder closure	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isLUB_of_mem_nhds Filter.mem_principal_self inf_comm ClusterPt.eq_1 mem_closure_iff_clusterPt
isLUB_of_mem_nhds 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter Filter.instMembership	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	not_lt Filter.inter_mem_inf IsOpen.mem_nhds isOpen_lt' Filter.nonempty_of_mem lt_of_lt_of_le lt_irrefl
lowerClosure_eq_Iic_csSup 📖	mathematical	Set.Nonempty BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	SetLike.coe LowerSet Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice LowerSet.instSetLike lowerClosure Set.Iic SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	upperClosure_eq_Ici_csInf instOrderTopologyOrderDual
upperClosure_eq_Ici_csInf 📖	mathematical	Set.Nonempty BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	SetLike.coe UpperSet Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice UpperSet.instSetLike upperClosure Set.Ici InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	Set.ext csInf_le_of_le IsGLB.mem_of_isClosed isGLB_csInf

---

← Back to Index