Theorems · Theorem · order theory

map_eq_top_iff

∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : LE α] [inst_2 : OrderTop α]
  [inst_3 : PartialOrder β] [inst_4 : OrderTop β] [OrderIsoClass F α β] (f : F) {a : α}, f a = ⊤ ↔ a = ⊤

Defined in

Mathlib.Order.Hom.Bounded

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound

Assumes

EquivLikeLEOrderTopPartialOrderOrderTopOrderIsoClass