ite_inter_closure_eq_of_inter_frontier_eq

English

If the intersections with frontier t are equal, then t.ite s s' intersect closure t equals s intersect closure t.

Русский

Если пересечения с границей frontier t равны, то (t.ite s s') ∩ closure t = s ∩ closure t.

LaTeX

$$$\bigl(t.ite s s'\bigr) \cap \overline{t} = s \cap \overline{t}$ given $s ∩ frontier t = s' ∩ frontier t$.$$

Lean4

theorem ite_inter_closure_eq_of_inter_frontier_eq (ht : s ∩ frontier t = s' ∩ frontier t) :
    t.ite s s' ∩ closure t = s ∩ closure t := by
  rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left, ite_inter_self,
    ite_inter_of_inter_eq _ ht]

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