subtypePermOfFintype_apply — Mathlib

English

The explicit value on a subtype element is the image under f with the predicate preserved.

Русский

Явное значение на элементе подтипа равно образу под действием f и сохранение предиката.

LaTeX

$$$(\\mathrm{subtypePermOfFintype}\, h)(x) = \\langle f x, h x x.2 \\rangle$$$

Lean4

@[simp]
theorem subtypePermOfFintype_apply (f : Perm α) {p : α → Prop} [Finite { x // p x }] (h : ∀ x, p x → p (f x))
    (x : { x // p x }) : subtypePermOfFintype f h x = ⟨f x, h x x.2⟩ :=
  rfl

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