ennreal.frontier_Iic

Stream: Is there code for X?

[Kalle Kytölä]

What is the right way of proving that the boundary of an Iic-interval up to a finite x : ennreal is the singleton {x}?

I.e.:

import topology.algebra.ordered.basic
import topology.instances.ennreal

open order set
open_locale topological_space nnreal ennreal

lemma ennreal.frontier_Iic_how (x : ℝ≥0∞) (hx : x ≠ ∞) :
  frontier (Iic x) = {x} := sorry

[Kalle Kytölä]

For comparison, in ℝ, the following is found by library_search:

import topology.algebra.ordered.basic
import topology.instances.ennreal

open order set
open_locale topological_space nnreal ennreal

lemma real.frontier_Iic_like_this (x : ℝ) :
  frontier (Iic x) = {x} := frontier_Iic

[Kalle Kytölä]

The reason frontier_Iic does not apply to ennreal is the assumption [no_top_order] in it. The assumption hx : x ≠ ∞ of course has mathematically "the same content".

[Kalle Kytölä]

Below is a super clumsy solution (but I believe in the right generality). I think such lemmas are important enough to include in mathlib (at least frontier_Ici in nnreal etc. would lead to similar issues), but my question is: what is the non-clumsy way to do these?

import topology.algebra.ordered.basic
import topology.instances.ennreal

open order set
open_locale topological_space nnreal ennreal

lemma compl_singleton_eq_Iio_union_Ioi {β : Type*} [topological_space β] [linear_order β]
  [order_topology β] [densely_ordered β] {b : β} :
  {b}ᶜ = Iio b ∪ Ioi b :=
by { ext x, simp, }

lemma interior_Iic' {β : Type*} [topological_space β] [linear_order β]
  [order_topology β] [densely_ordered β] {b : β} (h : ∃ c, b < c) :
  interior (Iic b) = Iio b :=
begin
  apply le_antisymm,
  { intros x hx,
    rw mem_interior_iff_mem_nhds at hx,
    by_cases hxb : x = b,
    { exfalso,
      rw hxb at hx,
      rcases exists_Ico_subset_of_mem_nhds hx h with ⟨v, ⟨hbv, hss⟩⟩,
      rcases exists_between hbv with ⟨z, hbz, hzv⟩,
      exact (lt_self_iff_false _).mp (lt_of_lt_of_le hbz (hss ⟨hbz.le, hzv⟩)), },
    rw ← Iic_diff_right,
    exact ⟨mem_of_mem_nhds hx, hxb⟩, },
  { apply interior_maximal Iio_subset_Iic_self is_open_Iio,
    exact order_topology.to_order_closed_topology, },
end

lemma frontier_Iic' {β : Type*} [topological_space β] [linear_order β]
  [order_topology β] [densely_ordered β] {b : β} (h : ∃ c, b < c) :
  frontier (Iic b) = {b} :=
begin
  apply compl_injective,
  rw [compl_frontier_eq_union_interior, compl_singleton_eq_Iio_union_Ioi],
  simp only [compl_Iic, interior_Ioi, interior_Iic],
  exact congr_arg (λ s, s ∪ (Ioi b)) (interior_Iic' h),
end

lemma ennreal.frontier_Iic (x : ℝ≥0∞) (hx : x ≠ ∞) :
  frontier (Iic x) = {x} :=
by { apply frontier_Iic' ⟨∞, lt_top_iff_ne_top.mpr hx⟩, }

[Kalle Kytölä]

I believe the relevant existing stuff should be around docs#frontier_Iic .

[Yury G. Kudryashov]

The proper way is to prove theorems like docs#closure_Ioi with assumption (Ioi x).nonempty.

[Yury G. Kudryashov]

You can either add new lemmas as prime versions or use h : (Ioi x).nonempty . some_tac, where some_tac tries to apply set.nonempty_Ioi and set.nonempty_Iio.

[Yury G. Kudryashov]

It looks like we have docs#closure_Ioi'

[Yury G. Kudryashov]

@[simp] lemma interior_Ici' {a : α} (ha : (Iio a).nonempty) : interior (Ici a) = Ioi a :=
let ⟨b, hb⟩ := ha in by rw [← compl_Iio, interior_compl, closure_Iio' hb, compl_Iic]


@[simp] lemma frontier_Ici' {a : α} (ha : (Iio a).nonempty) : frontier (Ici a) = {a} :=
by simp [frontier, ha]

[Yury G. Kudryashov]

The first proof can be simplified if you rewrite closure_Ioi' so that it assumes (Ioi a).nonempty

[Yury G. Kudryashov]

I'm not sure whether new lemmas should just replace the old ones or not.

[Kalle Kytölä]

Thank you very much! This looks great.

In the existing formulations, the typeclass [no_top_order] is really doing its work when it applies: I was super happy how smoothly (:= by library_search) the proof of frontier (Iic x) = {x} went in ℝ and ℝ≥0. I would therefore not want to remove the old ones, even if I think the new ones are needed as well.

I made a PR #10630 including both the Iic and Ici cases, with Yury's succinct proofs. [Edit: I guess I should include Iio and Ioi cases as well.]

[Kalle Kytölä]

By the way, I have not found documentation for the let ... in ... syntax, especially the in keyword in it. Any hints on where to look? I could not find it described in the #tpil nor at docs#tactic.interactive.let . By trial and error I figured the following would be essentially the same, right?

@[simp] lemma interior_Ici' {a : α} (ha : (Iio a).nonempty) : interior (Ici a) = Ioi a :=
by { cases ha with b hb, rw [← compl_Iio, interior_compl, closure_Iio' hb, compl_Iic], }

So is let X := Y in more or less the same as starting in tactic mode with cases Y with X and then continuing?

[Reid Barton]

let ... in ... is term mode syntax

[Reid Barton]

If X is a pattern, then it's like you say. Otherwise, it is like the let tactic

[Kalle Kytölä]

Ok, I think I only looked in #tpil tactics chapter, which makes no sense given that it is a term mode syntax. Searching for small words such as let and in is not easy, though. But I think I roughly got it now. Thanks!

[Yury G. Kudryashov]

I made a few comments. Please implement suggested changes, then change the label from awaiting-author to awaiting-review.

[Kalle Kytölä]

Thank you! I implemented the changes.

[Kalle Kytölä]

The "build mathlib" check now reports Build succeeded, but the file was noisy. I don't know what this means or how to fix it. Could someone help me understand what it is about?

(Btw, I didn't yet add the label "awaiting-review", since there is this failing check.)

[Kevin Buzzard]

It probably means that there is some blue output, e.g. a #check or non-terminal ring in the file somewhere.

[Kalle Kytölä]

Thank you! There was indeed a blue #lint at the end of the file :oops:.

[Yury G. Kudryashov]

I changed assumptions in more lemmas. Let's see if it compiles.

[Stuart Presnell]

Would it be possible to change this error message to make it more informative?

[Yury G. Kudryashov]

It's in scripts/detect_errors.py