# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: continuous_on.dif

#### Shing Tak Lam (Apr 14 2021 at 18:02):

Right now, I'm trying to prove that this triangular function $f : [0, 1] \to [0, 1]$ is continuous, but I'm struggling to find any lemmas which will help. I did find `continuous_on.if`

, but in my example it's a `dite`

and not an `ite`

, so it doesn't work. Does anyone have any suggestions on how to prove this? Or what `continuous_on.dif`

would look like?

```
import topology.unit_interval
open_locale unit_interval
noncomputable theory
lemma two_mul_mem_I {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ 1/2) : 2 * t ∈ I := ⟨by linarith, by linarith⟩
lemma two_sub_two_mul_mem_I {t : ℝ} (ht : (1/2 : ℝ) ≤ t) (ht' : t ≤ 1) : 2 - 2 * t ∈ I :=
⟨by nlinarith, by nlinarith⟩
def f : I → I := λ x,
if h : x.1 ≤ 1/2 then
⟨2 * x, two_mul_mem_I x.2.1 h⟩
else
⟨2 - 2 * x, two_sub_two_mul_mem_I (not_le.1 h).le x.2.2⟩
example : continuous f :=
begin
unfold f,
rw [continuous_iff_continuous_on_univ],
sorry
end
```

#### Eric Wieser (Apr 14 2021 at 19:49):

(docs#continuous_on.if for reference)

#### Eric Wieser (Apr 14 2021 at 19:58):

For your example, can't you solve it by moving the dite inside the angle brackets?

#### Floris van Doorn (Apr 14 2021 at 20:02):

Here is a generalization, but maybe not the most general form.

```
import topology.continuous_on
open set
variables {α β : Type*} [topological_space α] [topological_space β]
{p : α → Prop} [Π (a : α), decidable (p a)] {s : set α} {f g : α → β}
{t : set β}
theorem continuous_on.dif_subtype (hp : ∀ (a : α), a ∈ s ∩ frontier {a : α | p a} → f a = g a)
(hf : continuous_on f (s ∩ closure {a : α | p a}))
(hg : continuous_on g (s ∩ closure {a : α | ¬p a}))
(h2f : maps_to f {x | p x} t) (h2g : maps_to g {x | ¬ p x} t) :
continuous_on (λ x, if h : p x then (⟨f x, h2f h⟩ : t) else ⟨g x, h2g h⟩) s :=
sorry
```

It's about using `dite`

for functions that map into a subtype.

#### Floris van Doorn (Apr 14 2021 at 20:13):

Now with proof:

```
import topology.continuous_on
open set
variables {α β : Type*} [topological_space α] [topological_space β]
{p : α → Prop} [Π (a : α), decidable (p a)] {s : set α} {f g : α → β}
{t : set β}
theorem continuous_on.dif_subtype (hp : ∀ (a : α), a ∈ s ∩ frontier {a : α | p a} → f a = g a)
(hf : continuous_on f (s ∩ closure {a : α | p a}))
(hg : continuous_on g (s ∩ closure {a : α | ¬p a}))
(h2f : maps_to f {x | p x} t) (h2g : maps_to g {x | ¬ p x} t) :
continuous_on (λ x, if h : p x then (⟨f x, h2f h⟩ : t) else ⟨g x, h2g h⟩) s :=
begin
rw [embedding_subtype_coe.continuous_on_iff],
convert continuous_on.if hp hf hg,
ext x, split_ifs; simp [h]
end
```

#### Eric Wieser (Apr 14 2021 at 20:17):

Do we have a lemma that says `if h : p x then (⟨f x, h2f h⟩ : t) else ⟨g x, h2g h⟩ = ⟨if p x then f x else g x, _⟩`

for an appropriately valued underscore?

#### Floris van Doorn (Apr 14 2021 at 20:19):

`library_search`

couldn't easily find it (though I didn't let it terminate), so I'm not sure. The proof is just `split_ifs; simp [h]`

though.

#### Mario Carneiro (Apr 14 2021 at 20:21):

the proof in both senses

#### Shing Tak Lam (Apr 15 2021 at 04:37):

Eric Wieser said:

For your example, can't you solve it by moving the dite inside the angle brackets?

Oops, I've definitely #xy -ed myself here. That example didn't need a `dif`

, but I think for my use case I will need a `dif`

. The general statement I'm trying to prove is this, which I don't think you can write without a `dite`

?

```
import topology.unit_interval
open_locale unit_interval
example {X Y : Type} [topological_space X] [topological_space Y] (F G : X × ↥I → Y)
(hF : continuous F) (hG : continuous G)
-- hFG here is enough to show they agree on the appropriate `frontier`s with a bunch of other lemmas I have.
(hFG : ∀ x, F (x, ⟨1/2, sorry⟩) = G (x, ⟨1/2, sorry⟩)) :
continuous
(λ (x : X × ↥I),
dite (x.snd.val ≤ 1 / 2)
(λ (h : x.snd.val ≤ 1 / 2), F (x.fst, ⟨2 * x.snd.val, sorry⟩))
(λ (h : ¬x.snd.val ≤ 1 / 2), G (x.fst, ⟨2 * x.snd.val - 1, sorry⟩))) :=
begin
admit,
end
```

#### Shing Tak Lam (Apr 15 2021 at 05:24):

Floris van Doorn said:

Now with proof:

`import topology.continuous_on open set variables {α β : Type*} [topological_space α] [topological_space β] {p : α → Prop} [Π (a : α), decidable (p a)] {s : set α} {f g : α → β} {t : set β} theorem continuous_on.dif_subtype (hp : ∀ (a : α), a ∈ s ∩ frontier {a : α | p a} → f a = g a) (hf : continuous_on f (s ∩ closure {a : α | p a})) (hg : continuous_on g (s ∩ closure {a : α | ¬p a})) (h2f : maps_to f {x | p x} t) (h2g : maps_to g {x | ¬ p x} t) : continuous_on (λ x, if h : p x then (⟨f x, h2f h⟩ : t) else ⟨g x, h2g h⟩) s := begin rw [embedding_subtype_coe.continuous_on_iff], convert continuous_on.if hp hf hg, ext x, split_ifs; simp [h] end`

Unfortunately I've realised I've #xy -ed myself when making the example, so this can't be used as-is for my issue. But this is useful for some other things I'm doing. Thanks a lot!

#### Eric Wieser (Apr 15 2021 at 06:06):

Even with that example, the proof approach is probably to push the dite inside until it reaches the prop terms

#### Shing Tak Lam (Apr 15 2021 at 06:59):

Alright, thanks!

#### Floris van Doorn (Apr 15 2021 at 21:18):

Would a lemma like this be helpful?

```
import topology.continuous_on
open_locale topological_space
open set filter
variables {α β : Type*} [topological_space α] [topological_space β]
{p : α → Prop} [Π (a : α), decidable (p a)]
theorem continuous.dif
{f : {x // p x} → β} {g : {x // ¬ p x} → β}
(hp : ∀ (a ∈ frontier {a : α | p a}) (b : β),
tendsto f ((𝓝 a).comap coe) (𝓝 b) ↔ tendsto g ((𝓝 a).comap coe) (𝓝 b))
(hf : continuous f) (hg : continuous g) :
continuous (λ x, if h : p x then f ⟨x, h⟩ else g ⟨x, h⟩) :=
sorry
```

I'm not sure if this is the best way of saying that `f`

and `g`

agree on the frontier (I believe the hypothesis does state that, but I'm also not 100% sure about that).

Is it at all possible to reorganize your formalization so that `F`

and `G`

are defined on all `X × \R`

. Sometimes making a function total makes your life easier. You can still conder them as functions on `X × I`

, stating that they're only continuous on `X × I`

instead of everywhere.

Last updated: May 07 2021 at 21:10 UTC