coe_prodEquivOfClosedCompl — Mathlib

English

The canonical coercion of the prod equivalence matches the product isomorphism.

Русский

Каноническое отображение произведения совпадает с изоморфизмом произведения.

LaTeX

$$$$ \text{coe}_{prodEquivClosedCompl} = \text{prodEquivIsCompl} $$$$

Lean4

@[simp]
theorem coe_prodEquivOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E)) (hq : IsClosed (q : Set E)) :
    ⇑(p.prodEquivOfClosedCompl q h hp hq) = p.prodEquivOfIsCompl q h :=
  rfl

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