prod_eq_prod_of_nonempty' — Mathlib

English

As above, but with the nonempty source condition applied to the swapped product: (eX'.prod eY').source.Nonempty implies eX.prod eY = eX'.prod eY' iff eX = eX' ∧ eY = eY'.

Русский

Как выше, но условие непустоты источника применяется к swapped-продукту: Nonempty (eX'.prod eY').source ⇒ eX.prod eY = eX'.prod eY' ⇔ eX = eX' ∧ eY = eY'.

LaTeX

$$$ (eX'.prod eY').source.Nonempty \Rightarrow (eX.prod eY = eX'.prod eY' \Leftrightarrow eX = eX' \wedge eY = eY') $$$

Lean4

theorem prod_eq_prod_of_nonempty' {eX eX' : OpenPartialHomeomorph X X'} {eY eY' : OpenPartialHomeomorph Y Y'}
    (h : (eX'.prod eY').source.Nonempty) : eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY' := by
  rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY']

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