preimage_coe_eq_empty — Mathlib

English

Let s and t be subsets of a set A. The set of elements of s that also lie in t, viewed as a subset of s, is empty if and only if s and t are disjoint.

Русский

Пусть s и t — подмножества множества A. Множество элементов s, которые одновременно принадлежат t, как подмножество s, пусто тогда и только тогда, когда s и t не пересекаются.

LaTeX

$$$\{x \in s \mid x \in t\} = \emptyset \iff s \cap t = \emptyset$$$

Lean4

theorem preimage_coe_eq_empty {s t : Set α} : ((↑) : s → α) ⁻¹' t = ∅ ↔ s ∩ t = ∅ := by
  simp [← not_nonempty_iff_eq_empty, preimage_coe_nonempty]
    -- Not `@[simp]` since `simp` can prove this.

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