Zulip Chat Archive

Stream: Is there code for X?

Topic: Extending intervals

Stuart Presnell (Jul 12 2022 at 13:07):

We have lemmas like Ico_insert_right (h : a ≤ b) : insert b (Ico a b) = Icc a b for extending open intervals to closed intervals, but do we also have lemmas for extending closed intervals by inserting the next element? For example, 

example (n : ℕ) : Ioc 0 n.succ = insert n.succ (Ioc 0 n) :=
begin
  rcases n.eq_zero_or_pos with rfl | hn, { simp },
  simp_rw [←Ico_succ_succ, Ico_insert_right (succ_le_succ hn.le), Ico_succ_right],
end

Yury G. Kudryashov (Jul 12 2022 at 13:08):

We have something like that for succ_orders

Yaël Dillies (Jul 12 2022 at 13:08):

There's also a bunch missing that I'm PRing soon.

Yury G. Kudryashov (Jul 12 2022 at 13:09):

See docs#order.Icc_succ_right

Yury G. Kudryashov (Jul 12 2022 at 13:09):

Unfortunately, nat.succ is not syntactically equal to order.succ

Yury G. Kudryashov (Jul 12 2022 at 13:10):

But they're definitionally equal.

Stuart Presnell (Jul 12 2022 at 13:13):

We also don't appear to have [succ_order ℕ]

Yaël Dillies (Jul 12 2022 at 13:13):

docs#nat.succ_order

Stuart Presnell (Jul 12 2022 at 13:14):

So why does have := @order.Ioc_succ_right ℕ _ _ give

failed to synthesize type class instance for
n : ℕ
⊢ succ_order ℕ

Yaël Dillies (Jul 12 2022 at 13:14):

Well, are you importing data.nat.succ_pred?

Stuart Presnell (Jul 12 2022 at 13:16):

Just added the import of import data.nat.succ_pred

Stuart Presnell (Jul 12 2022 at 13:22):

Sorry, continuing to be stupid: is there a version of Ioc_succ_right for finset.Ioc rather than set.Ioc?

Yaël Dillies (Jul 12 2022 at 13:27):

No, this is part of what I'm adding soon.

Last updated: Dec 20 2023 at 11:08 UTC