sumElim_of_separatedNhds — Mathlib

English

If f and g are embeddings and the ranges are separated in the nhds sense (SeparatedNhds), then Sum.elim f g is an embedding.

Русский

Если f и g — вложения, и множества их образов разделены в смысле nhds, тогда Sum.elim f g — вложение.

LaTeX

$$$\\text{IsEmbedding}(\\mathrm{Sum.elim}\ f\ g) \\iff \\text{IsEmbedding}(f) ∧ \\text{IsEmbedding}(g) ∧ \\text{SeparatedNhds}(\\mathrm{range}(f), \\mathrm{range}(g))$$$

Lean4

theorem sumElim_of_separatedNhds (hf : IsInducing f) (hg : IsInducing g) (hsep : SeparatedNhds (range f) (range g)) :
    IsInducing (Sum.elim f g) :=
  hf.sumElim hg hsep.disjoint_closure_left hsep.disjoint_closure_right

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