ite_inter_closure_compl_eq_of_inter_frontier_eq

English

If s ∩ frontier t = s' ∩ frontier t, then (t.ite s s') ∩ closure tᶜ = s' ∩ closure tᶜ.

Русский

Если s ∩ frontier t = s' ∩ frontier t, тогда (t.ite s s') ∩ closure tᶜ = s' ∩ closure tᶜ.

LaTeX

$$$\bigl(t.ite s s'\bigr) \cap \overline{t^c} = s' \cap \overline{t^c}$ при равенстве границ.$$

Lean4

theorem ite_inter_closure_compl_eq_of_inter_frontier_eq (ht : s ∩ frontier t = s' ∩ frontier t) :
    t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ :=
  by
  rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq]
  rwa [frontier_compl, eq_comm]

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