Theorems · Theorem · order theory

Order.IsNormal.exists_map_le_lt_map_succ_of_exists_ge

∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : SuccOrder α] [inst_3 : LinearOrder β]
  [NoMaxOrder α] [inst_5 : OrderBot α] [WellFoundedLT β] {f : α → β} {x : β},
  Order.IsNormal f → (∃ y, x ≤ f y) → f ⊥ ≤ x → ∃ a, f a ≤ x ∧ x < f (Order.succ a)

Defined in: Mathlib.Order.IsNormal
Cited by: 1 results in Mathlib
Foundations: Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: LinearOrder WellFoundedLT SuccOrder LinearOrder NoMaxOrder OrderBot WellFoundedLT

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites22

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.preimageproof · cited by 4,946
Bot.botstatement and proof · cited by 4,720
LE.le.transproof · cited by 3,151
le_reflproof · cited by 2,061
Set.Iicproof · cited by 1,111
OrderBotstatement and proof · cited by 1,055
SupSet.sSupproof · cited by 954
Order.succstatement · cited by 633
BddAboveproof · cited by 620
SuccOrderstatement and proof · cited by 574
WellFoundedLTstatement and proof · cited by 491

Cited by1

Results whose statement or proof uses this declaration.

Order.IsNormal.exists_map_le_lt_map_succproof · cited by 0