preimage_coe_nonempty — Mathlib

English

The preimage of t under Subtype.val is nonempty iff s ∩ t is nonempty.

Русский

Предобраз Subtype.val множества t непуст тогда и только тогда, когда s ∩ t непуст.

LaTeX

$$$ \operatorname{Nonempty}( ((\uparrow) : s \to \alpha)^{-1}(t) ) \iff \operatorname{Nonempty}(s \cap t). $$$

Lean4

theorem preimage_coe_nonempty {s t : Set α} : (((↑) : s → α) ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty := by
  rw [← image_preimage_coe, image_nonempty]

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