preimage_coe_compl — Mathlib

English

For every subset s of A, the preimage of its complement under the inclusion map s → A is empty.

Русский

Для любого подмножества s множества A прообраз его дополнения по включающему отображению s → A равен пустому множеству.

LaTeX

$$$\{ x \in s \mid x \in s^{c} \} = \emptyset$$$

Lean4

theorem preimage_coe_compl (s : Set α) : ((↑) : s → α) ⁻¹' sᶜ = ∅ :=
  preimage_coe_eq_empty.2 (inter_compl_self s)

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