Theorems · Theorem · logic and foundations

Filter.EventuallyConst.of_monotone_of_lt_cof

∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f →
    Cardinal.lift.{u, v} (Cardinal.mk β) < Cardinal.lift.{v, u} (Order.cof α) → Filter.EventuallyConst f Filter.atTop

Defined in: Mathlib.SetTheory.Cardinal.EventuallyConst
Cited by: 3 results in Mathlib
Foundations: Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: LinearOrder PartialOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites24

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

LinearOrderstatement and proof · cited by 8,572
Set.Elemproof · cited by 7,166
PartialOrderstatement and proof · cited by 6,410
Set.rangeproof · cited by 4,705
LE.le.transproof · cited by 3,151
Cardinalstatement and proof · cited by 2,598
Filter.atTopstatement · cited by 2,405
Monotonestatement and proof · cited by 1,397
Cardinal.mkstatement and proof · cited by 942
Cardinal.liftstatement and proof · cited by 583
Filter.EventuallyConststatement · cited by 93
Order.cofstatement and proof · cited by 86

Cited by3

Results whose statement or proof uses this declaration.

Ordinal.eventuallyConst_of_monotoneproof · cited by 1
Cardinal.eventuallyConst_of_monotoneproof · cited by 1
Filter.EventuallyConst.of_antitone_of_lt_cofproof · cited by 0