ofSubtype_apply_mem_iff_mem — Mathlib

English

For any a ∈ α, applying the inclusion map and then checking p is equivalent to checking p at a, i.e., p((ofSubtype f) a) holds iff p(a) holds.

Русский

Для любого a: p((ofSubtype f) a) эквивалентно p(a).

LaTeX

$$$ p((\\mathrm{ofSubtype}\\, f)\\, a) \\iff p(a) $$$

Lean4

theorem ofSubtype_apply_mem_iff_mem (f : Perm (Subtype p)) (x : α) : p ((ofSubtype f : α → α) x) ↔ p x :=
  if h : p x then by simpa only [h, iff_true, MonoidHom.coe_mk, ofSubtype_apply_of_mem f h] using (f ⟨x, h⟩).2
  else by simp [h, ofSubtype_apply_of_not_mem f h]

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