exists_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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