Zulip Chat Archive
Stream: mathlib4
Topic: simpNF
Johan Commelin (Jan 13 2023 at 14:46):
Johan Commelin (Jan 13 2023 at 14:47):
simp seems to be doing pretty wicked things, if it proves sup_s_one using sup_s_zero.
Johan Commelin (Jan 13 2023 at 14:47):
-- Porting note: Use something like `@[to_additive (attr := simp)]` instead.
-- However, this makes a simpNF error like:
-- `supₛ_one` can be proved like `by simp only [@supₛ_zero]`
-- So the `simp` attribute is written below the definition.
@[to_additive]
theorem supₛ_one : supₛ (1 : Set α) = 1 :=
attribute [simp] supₛ_zero
attribute [simp] supₛ_one
Eric Wieser (Jan 13 2023 at 15:29):
What's the statement of supₛ_zero that it generates?
Jihoon Hyun (Jan 13 2023 at 15:36):
It is supₛ (0 : Set α) = 0.
Last updated: Dec 20 2023 at 11:08 UTC