English
Let s, u, v ⊆ α with s ⊆ u ∪ v and s ∩ (u ∩ v) = ∅. Then the preimage of u under the inclusion s → α equals the complement (in s) of the preimage of v under the inclusion: (↑)^{-1}(u) = (↑)^{-1}(v)^{c}.
Русский
Пусть s ⊆ α и u, v ⊆ α удовлетворяют s ⊆ u ∪ v и s ∩ (u ∩ v) = ∅. Тогда предобраз u по включению s → α равен дополнению предобраза v по той же включению внутри s.
LaTeX
$$$ ((\\uparrow) : s \\to \\alpha)^{-1}(u) = ((↑)^{-1}(v))^{c} \\quad\\text{given } s \\subseteq u \\cup v \\text{ and } s \\cap (u \\cap v) = \\emptyset. $$$
Lean4
theorem preimage_subtype_coe_eq_compl {s u v : Set α} (hsuv : s ⊆ u ∪ v) (H : s ∩ (u ∩ v) = ∅) :
((↑) : s → α) ⁻¹' u = ((↑) ⁻¹' v)ᶜ := by
ext ⟨x, x_in_s⟩
constructor
· intro x_in_u x_in_v
exact eq_empty_iff_forall_notMem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩
· grind
