single_trans_of_mem — Mathlib

English

If element c belongs to the image of b under the PEquiv f, then the transitive action on single elements preserves equivalence to c.

Русский

Если элемент c принадлежит образу b под PEquiv f, то переход между единичными элементами сохраняет эквивалентность к c.

LaTeX

$$$\\forall a\\;{b}\\;{c}\\;{f} : {β} \\simeq.{γ},\\; c \\in f(b) \\Rightarrow (\\mathrm{single}\\ a\\ b).trans f = \\mathrm{single}\\ a\\ c$$$

Lean4

theorem single_trans_of_mem (a : α) {b : β} {c : γ} {f : β ≃. γ} (h : c ∈ f b) : (single a b).trans f = single a c :=
  by
  ext
  dsimp [single, PEquiv.trans]
  split_ifs <;> simp_all

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