inter_eq_of_inter_eq_of_eqOn — Mathlib

English

If e.IsImage s t and e'.IsImage s t, and e.source ∩ s = e'.source ∩ s and EqOn e e' (e.source ∩ s), then e.target ∩ t = e'.target ∩ t.

Русский

Если IsImage(e, s, t) и IsImage(e', s, t), и e.source ∩ s = e'.source ∩ s, и EqOn e e' на (e.source ∩ s), тогда e.target ∩ t = e'.target ∩ t.

LaTeX

$$IsImage(e, s, t) \\land IsImage(e', s, t) \\land (e.source \\cap s) = (e'.source \\cap s) \\land EqOn(e, e', e.source \\cap s) \\Rightarrow e.target \\cap t = e'.target \\cap t$$

Lean4

theorem inter_eq_of_inter_eq_of_eqOn {e' : OpenPartialHomeomorph X Y} (h : e.IsImage s t) (h' : e'.IsImage s t)
    (hs : e.source ∩ s = e'.source ∩ s) (Heq : EqOn e e' (e.source ∩ s)) : e.target ∩ t = e'.target ∩ t :=
  h.toPartialEquiv.inter_eq_of_inter_eq_of_eqOn h' hs Heq

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