English
There exists an ExistsAddOfLE structure on WithTop α provided LE α, Add α, and ExistsAddOfLE α.
Русский
Существует структура ExistsAddOfLE на WithTop α при наличии LE α, Add α и ExistsAddOfLE α.
LaTeX
$$$[LE \\\\alpha] [Add \\\\alpha] [ExistsAddOfLE \\\\alpha] : ExistsAddOfLE (WithTop \\\\alpha)$$$
Lean4
instance existsAddOfLE [LE α] [Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithTop α) :=
⟨fun {a} {b} =>
match a, b with
| ⊤, ⊤ => by simp
| (a : α), ⊤ => fun _ => ⟨⊤, rfl⟩
| (a : α), (b : α) => fun h =>
by
obtain ⟨c, rfl⟩ := exists_add_of_le (WithTop.coe_le_coe.1 h)
exact ⟨c, rfl⟩
| ⊤, (b : α) => fun h => (not_top_le_coe _ h).elim⟩
-- instance canonicallyOrderedAddCommMonoid [CanonicallyOrderedAddCommMonoid α] :
-- CanonicallyOrderedAddCommMonoid (WithTop α) :=
-- { WithTop.orderBot, WithTop.orderedAddCommMonoid, WithTop.existsAddOfLE with
-- le_self_add := fun a b =>
-- match a, b with
-- | ⊤, ⊤ => le_rfl
-- | (a : α), ⊤ => le_top
-- | (a : α), (b : α) => WithTop.coe_le_coe.2 le_self_add
-- | ⊤, (b : α) => le_rfl }
--
-- instance [CanonicallyLinearOrderedAddCommMonoid α] :
-- CanonicallyLinearOrderedAddCommMonoid (WithTop α) :=
-- { WithTop.canonicallyOrderedAddCommMonoid, WithTop.linearOrder with }
