English
If s and s' are open and the frontier of t has the property that membership in s and s' agrees on the frontier, then t.ite s s' is open.
Русский
Если s и s' открыты и по границе frontier выполнено условие согласования принадлежности к s и к s', то t.ite s s' открыто.
LaTeX
$$$\text{IsOpen}(t.ite s s')$ given the frontier coherence condition.$$
Lean4
theorem ite' (hs : IsOpen s) (hs' : IsOpen s') (ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s') : IsOpen (t.ite s s') := by
classical
simp only [isOpen_iff_continuous_mem, Set.ite] at *
convert continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2
rename_i x
by_cases hx : x ∈ t <;> simp [hx]
