Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 7e69148

Browse files
committed
feat(order/conditionally_complete_lattice): Make cSup_empty a simp lemma (#13318)
1 parent 159855d commit 7e69148

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/order/conditionally_complete_lattice.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -674,10 +674,10 @@ section conditionally_complete_linear_order_bot
674674

675675
variables [conditionally_complete_linear_order_bot α]
676676

677-
lemma cSup_empty : (Sup ∅ : α) = ⊥ :=
677+
@[simp] lemma cSup_empty : (Sup ∅ : α) = ⊥ :=
678678
conditionally_complete_linear_order_bot.cSup_empty
679679

680-
lemma csupr_of_empty [is_empty ι] (f : ι → α) : (⨆ i, f i) = ⊥ :=
680+
@[simp] lemma csupr_of_empty [is_empty ι] (f : ι → α) : (⨆ i, f i) = ⊥ :=
681681
by rw [supr_of_empty', cSup_empty]
682682

683683
@[simp] lemma csupr_false (f : false → α) : (⨆ i, f i) = ⊥ := csupr_of_empty f

0 commit comments

Comments
 (0)