coe_image — Mathlib

English

The image of a subset s of a subtype p under the coercion to α equals the set {x | ∃ h, p x ∧ ⟨x,h⟩ ∈ s}.

Русский

Образ подмножества s ⊆ подтипа p при включении в α равен множеству {x | существует доказательство p x и ⟨x,h⟩ ∈ s}.

LaTeX

$$$ (\uparrow) '' s = \{ x \mid \exists h : p x, (\langle x,h\rangle : Subtype p) \in s \}$$$

Lean4

theorem coe_image {p : α → Prop} {s : Set (Subtype p)} : (↑) '' s = {x | ∃ h : p x, (⟨x, h⟩ : Subtype p) ∈ s} :=
  Set.ext fun a => ⟨fun ⟨⟨_, ha'⟩, in_s, h_eq⟩ => h_eq ▸ ⟨ha', in_s⟩, fun ⟨ha, in_s⟩ => ⟨⟨a, ha⟩, in_s, rfl⟩⟩

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