ofEquiv_F — Mathlib

English

Let F be a realizer and E: F.σ ≃ τ a realizer. Then for every s in τ, the transported realizer satisfies ((F.ofEquiv E).F)(s) = F.F(E.symm s).

Русский

Пусть F — реализатор, а E: F.σ ≃ τ. Тогда для каждого элемента s из τ перенесенный реализатор удовлетворяет (F.ofEquiv E).F(s) = F.F(E.symm s).

LaTeX

$$$ \forall s, \; (F.ofEquiv E).F(s) = F.F(E.symm(s)). $$$$

Lean4

@[simp]
theorem ofEquiv_F (F : Realizer α) (E : F.σ ≃ τ) (s : τ) : (F.ofEquiv E).F s = F.F (E.symm s) := by delta ofEquiv; simp

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