ite — Mathlib

English

If s and s' are open and the frontier equality holds on t, then t.ite s s' is open.

Русский

Если s и s' открыты и выполняется равенство границы frontier на t, тогда t.ite s s' открыто.

LaTeX

$$$\text{IsOpen}(s) \to \text{IsOpen}(s') \to (s\cap \partial t = s'\cap \partial t) \Rightarrow \text{IsOpen}(t.ite s s').$$$

Lean4

theorem ite (hs : IsOpen s) (hs' : IsOpen s') (ht : s ∩ frontier t = s' ∩ frontier t) : IsOpen (t.ite s s') :=
  hs.ite' hs' fun x hx => by simpa [hx] using Set.ext_iff.1 ht x

Похожие утверждения