refl_prod_refl — Mathlib

English

A simplicial equality: the product of identity open partial homeomorphisms equals the identity on the product space, in a simplified form.

Русский

Симплайсовое равенство: произведение тождественных открытых частичных гомеоморфизмов равно тождественному отображению на произведении пространств.

LaTeX

$$$ OpenPartialHomeomorph.refl X \; .prod\; OpenPartialHomeomorph.refl Y = OpenPartialHomeomorph.refl (X \times Y) $$$

Lean4

@[simp]
theorem refl_prod_refl :
    (OpenPartialHomeomorph.refl X).prod (OpenPartialHomeomorph.refl Y) = OpenPartialHomeomorph.refl (X × Y) :=
  OpenPartialHomeomorph.ext _ _ (fun _ => rfl) (fun _ => rfl) univ_prod_univ

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