eq_preimage_subtype_val_iff — Mathlib

English

Let p be a predicate on α, s ⊆ Subtype p and t ⊆ α. Then s equals the preimage of t under the projection Subtype.val if and only if for all x with p(x), ⟨x, h⟩ ∈ s ↔ x ∈ t.

Русский

Пусть p(x) — предикат на α, s ⊆ Subtype p, t ⊆ α. Тогда s равно обратному образу t при проекции Subtype.val тогда и только если для всех x с p(x) верно ⟨x, h⟩ ∈ s ⇔ x ∈ t.

LaTeX

$$$ s = \\operatorname{Subtype.val}^{-1}(t) \\iff \\forall x (h : p(x)), (\\langle x,h \\rangle : \\text{Subtype } p) \\in s \\iff x \\in t. $$$

Lean4

theorem eq_preimage_subtype_val_iff {p : α → Prop} {s : Set (Subtype p)} {t : Set α} :
    s = Subtype.val ⁻¹' t ↔ ∀ (x) (h : p x), (⟨x, h⟩ : Subtype p) ∈ s ↔ x ∈ t := by grind

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