subtypeEquivRight_apply — Mathlib

English

For predicates p and q with ∀ x, p x ↔ q x and any e proving the pointwise equivalence, the forward map of the right-subtype equivalence sends z : { x : α // p x } to ⟨ z.1, (e z.1).mp z.2 ⟩.

Русский

Для предикатов p, q с ∀ x, p x ↔ q x и любого e, доказывающего равенство по точкам, отображение вправо задающее эквивалентность подтипов монтирует z : { x : α // p x } в ⟨ z.1, (e z.1).mp z.2 ⟩.

LaTeX

$$$( \\forall x, p x \\leftrightarrow q x ) \\Rightarrow ( (\\mathrm{subtypeEquivRight}\\ e)\\ z = \\langle z.1, (e z.1).mp z.2 \\rangle )$$$

Lean4

theorem subtypeEquivRight_apply {p q : α → Prop} (e : ∀ x, p x ↔ q x) (z : { x // p x }) :
    subtypeEquivRight e z = ⟨z, (e z.1).mp z.2⟩ :=
  rfl

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