subtypePerm — Mathlib

English

ExtendDomain_eq_one_iff: e.extendDomain f = 1 iff e = 1 (simp).

Русский

ExtendDomain_eq_one_iff: e.extendDomain f = 1 эквивалентно e = 1 (simp).

LaTeX

$$$e \extendDomain f = 1 \iff e = 1$$$

Lean4

/-- If the permutation `f` fixes the subtype `{x // p x}`, then this returns the permutation
  on `{x // p x}` induced by `f`. -/
def subtypePerm (f : Perm α) (h : ∀ x, p (f x) ↔ p x) : Perm { x // p x }
    where
  toFun := fun x => ⟨f x, (h _).2 x.2⟩
  invFun := fun x => ⟨f⁻¹ x, (h (f⁻¹ x)).1 <| by simpa using x.2⟩
  left_inv _ := by simp only [Perm.inv_apply_self, Subtype.coe_eta]
  right_inv _ := by simp only [Perm.apply_inv_self, Subtype.coe_eta]

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