preimage_coe_compl' — Mathlib

English

For any subset s of A, the preimage of s under the inclusion from sᶜ to A is empty; equivalently, s ∩ sᶜ = ∅.

Русский

Для любого подмножества s множества A прообраз включения из sᶜ в A равен пустому множеству; эквивалентно s ∩ sᶜ = ∅.

LaTeX

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

Lean4

@[simp]
theorem preimage_coe_compl' (s : Set α) : (fun x : (sᶜ : Set α) => (x : α)) ⁻¹' s = ∅ :=
  preimage_coe_eq_empty.2 (compl_inter_self s)

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