closed interval not neighborhood of edge

Stream: Is there code for X?

[llllvvuu]

I tried a few spellings, nothing came up for exact?/apply?/aesop?/etc:

import Mathlib

open scoped Topology

lemma foo {a b : ℝ} : Set.Icc a b ∉ 𝓝 a := by
  by_contra hc
  obtain ⟨ε, ε_pos, ε_in_icc⟩ := Metric.mem_nhds_iff.mp hc
  have h_mem : a - ε/2 ∈ Metric.ball a ε := mem_ball_iff_norm'.mpr (by simp [ε_pos, abs_of_pos])
  have h_nmem : a - ε/2 ∉ Set.Icc a b := Set.not_mem_Icc_of_lt (by linarith)
  exact h_nmem (ε_in_icc h_mem)

lemma bar {a b c : ℝ} : Set.Icc a b ∈ 𝓝 c ↔ a < c ∧ c < b := by
  constructor
  · sorry
  · exact fun ⟨h1, h2⟩ ↦ Icc_mem_nhds h1 h2

lemma baz {a b c : ℝ} : Set.Icc a b ∈ 𝓝 c ↔ Set.Ioo a b ∈ 𝓝 c := by
  constructor
  · sorry
  · exact fun h ↦ Filter.mem_of_superset h Set.Ioo_subset_Icc_self

Do we have something like this?

[Patrick Massot]

I would be surprised if this is in Mathlib. They look pretty useless. What are you trying to do with those lemmas?

[llllvvuu]

I have (not #mwe unfortunately):

def Rectangle (z w : ℂ) : Set ℂ := [[z.re, w.re]] ×ℂ [[z.im, w.im]]

lemma RectanglePullToNhdOfPole' {f : ℂ → ℂ} {z₀ z₁ z₂ z₃ p : ℂ}
    -- ...
    (hp : Rectangle z₁ z₂ ∈ 𝓝 p) (hz : Rectangle z₁ z₂ ⊆ Rectangle z₀ z₃)
    (fHolo : HolomorphicOn f (Rectangle z₀ z₃ \ {p})) :
    RectangleIntegral f z₀ z₃ = RectangleIntegral f z₁ z₂ := by
  sorry

and I need p to not be on the edge of the inner rectangle. But maybe I should take instead of (hp : Rectangle z₁ z₂ ∈ 𝓝 p), just directly (hp : z₁ < p.re ∧ ...)?

[Junyan Xu]

import Mathlib

open scoped Topology

lemma bar {a b c : ℝ} : Set.Icc a b ∈ 𝓝 c ↔ a < c ∧ c < b := by
  rw [← mem_interior_iff_mem_nhds, interior_Icc]; rfl

lemma foo {a b : ℝ} : Set.Icc a b ∉ 𝓝 a := by
  rw [bar]; exact (irrefl _ ·.1)

lemma baz {a b c : ℝ} : Set.Icc a b ∈ 𝓝 c ↔ Set.Ioo a b ∈ 𝓝 c := by
  rw [← interior_Icc]; exact interior_mem_nhds.symm

[Yury G. Kudryashov]

bar above looks like a reasonable simp lemma for mathlib, probably with Ioo spelling on the right.

[llllvvuu]

https://github.com/leanprover-community/mathlib4/pull/11178