exists_right — Mathlib

English

If x ≃ y, then for every j in y there exists i in x such that x.Func(i) ≃ y.Func(j).

Русский

Если x эквивалентно y, то для каждого j из y существует i из x такое, что x.Func(i) эквивалентно y.Func(j).

LaTeX

$$$Equiv(x,y) \Rightarrow \forall j : y.Type, \exists i : x.Type, (x.Func i) \Equiv (y.Func j)$$$

Lean4

theorem exists_right {x y : PSet} (h : Equiv x y) : ∀ j, ∃ i, Equiv (x.Func i) (y.Func j) :=
  (equiv_iff.1 h).2

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