Mathlib Map

Theorems · Theorem · order theory

WithTop.range_coe

∀ {α : Type u_1} [inst : Preorder α], Set.range WithTop.some = Set.Iio ⊤
Defined in
Mathlib.Order.Interval.Set.WithBotTop
Cited by
19 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext, Quot.sound
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

WithTop.image_coe_Iic · cited by 4WithTop.image_coe_IicWithTop.image_coe_Iio · cited by 4WithTop.image_coe_IioWithTop.image_coe_Icc · cited by 3WithTop.image_coe_IccWithTop.image_coe_Ico · cited by 3WithTop.image_coe_IcoWithTop.image_coe_Ioc · cited by 3WithTop.image_coe_IocWithTop.image_coe_Ioo · cited by 3WithTop.image_coe_IooWithTop.preimage_coe_Iio_top · cited by 3WithTop.preimage_coe_Iio_…WithTop.isEmbedding_coe · cited by 2WithTop.isEmbedding_coeENNReal.range_coe' · cited by 2ENNReal.range_coe'WithTop.image_coe_Ici · cited by 2WithTop.image_coe_IciENat.range_natCast · cited by 2ENat.range_natCastWithTop.image_coe_Ioi · cited by 2WithTop.image_coe_IoiWithTop.isOpenEmbedding_coe · cited by 1WithTop.isOpenEmbedding_c…WithTop.tendsto_nhds_top_iff · cited by 1WithTop.tendsto_nhds_top_…WithTop.coe_covBy_coe · cited by 0WithTop.coe_covBy_coeSet · cited by 53352SetTop.top · cited by 9680Top.topPreorder · cited by 7952PreorderSet.range · cited by 4705Set.rangeWithTop · cited by 3754WithTopSet.ext · cited by 2266Set.extSet.Iio · cited by 1166Set.IioWithTop.some · cited by 1128WithTop.someWithTop.range_coeCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Top.topstatement · cited by 9,680
  • Preorderstatement and proof · cited by 7,952
  • Set.rangestatement · cited by 4,705
  • WithTopstatement and proof · cited by 3,754
  • Set.extproof · cited by 2,266
  • Set.Iiostatement · cited by 1,166
  • WithTop.somestatement and proof · cited by 1,128

Cited by19

Results whose statement or proof uses this declaration.