Theorems · Theorem · general topology
Filter.Ioi_mem_atTop
∀ {α : Type u_3} [inst : Preorder α] [NoTopOrder α] (x : α), Set.Ioi x ∈ Filter.atTop- Defined in
- Mathlib.Order.Filter.AtTopBot.Defs
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Quot.sound
- Assumes
- PreorderNoTopOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Filterstatement · cited by 8,121
- Preorderstatement and proof · cited by 7,952
- Set.ofPredproof · cited by 6,101
- LE.le.transproof · cited by 3,151
- Filter.atTopstatement and proof · cited by 2,405
- Set.Ioistatement and proof · cited by 1,463
- Filter.mem_of_supersetproof · cited by 308
- Filter.inter_memproof · cited by 153
- NoTopOrderstatement and proof · cited by 50
- lt_of_le_not_geproof · cited by 33
- Filter.mem_atTopproof · cited by 9
Cited by36
Results whose statement or proof uses this declaration.
- Filter.eventually_gt_atTopproof · cited by 90
- MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendstoproof · cited by 5
- UpperHalfPlane.tendsto_comap_im_ofComplexproof · cited by 5
- hasSum_choose_mul_geometric_of_norm_lt_one'proof · cited by 4
- MeasureTheory.integrableOn_Ioi_deriv_of_nonnegproof · cited by 3
- tendsto_rpow_neg_atTopproof · cited by 3
- Filter.EventuallyEq.div_mul_cancel_atTopproof · cited by 3
- tendsto_atTop_of_mapClusterPtproof · cited by 3
- Hyperreal.lt_of_tendsto_atTopproof · cited by 3
- MeasureTheory.integral_deriv_smul_comp_Ioiproof · cited by 2
- UpperHalfPlane.differentiableAt_cuspFunctionproof · cited by 2
- not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioiproof · cited by 2