setSubtypeComm_apply — Mathlib

English

The forward map sends a subset s of the subtype {a // p a} to the pair consisting of the set {a | ∃ h : p a, ⟨a,h⟩ ∈ s} and the proof that ∀ a ∈ that set, p a.

Русский

Прямое отображение отправляет подмножество s подтипа {a // p a} в пару, состоящую из множества {a | ∃ h : p a, ⟨a,h⟩ ∈ s} и доказательства, что ∀ a ∈ это множество, p a.

LaTeX

$$$ (Equiv.setSubtypeComm\\, p)(s) = \\langle \\{ a : α \\mid ∃ h : p a, ⟨a,h⟩ ∈ s \\}, \\; \\ldots \\rangle $$$

Lean4

@[simp]
protected theorem setSubtypeComm_apply (p : α → Prop) (s : Set { a // p a }) :
    (Equiv.setSubtypeComm p) s = ⟨{a | ∃ h : p a, ⟨a, h⟩ ∈ s}, fun _ h ↦ h.1⟩ :=
  rfl

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