English
If p is a decidable predicate that separates s and t by p on s and not p on t, then s ∪ t is bijective to s ⊕ t.
Русский
Пусть p — разрешимый предикат, который разделяет множества s и t так, что p(x) выполняется на x ∈ s, а для x ∈ t p(x) ложно; тогда s ∪ t эквивалентно s ⊕ t.
LaTeX
$$$(s \cup t : \mathrm{Set}\,\alpha) \cong s \oplus t$$$
Lean4
/-- If sets `s` and `t` are separated by a decidable predicate, then `s ∪ t` is equivalent to
`s ⊕ t`. -/
protected def union' {α} {s t : Set α} (p : α → Prop) [DecidablePred p] (hs : ∀ x ∈ s, p x) (ht : ∀ x ∈ t, ¬p x) :
(s ∪ t : Set α) ≃ s ⊕ t
where
toFun
x :=
if hp : p x then Sum.inl ⟨_, x.2.resolve_right fun xt => ht _ xt hp⟩
else Sum.inr ⟨_, x.2.resolve_left fun xs => hp (hs _ xs)⟩
invFun
o :=
match o with
| Sum.inl x => ⟨x, Or.inl x.2⟩
| Sum.inr x => ⟨x, Or.inr x.2⟩
left_inv := fun ⟨x, h'⟩ => by by_cases h : p x <;> simp [h]
right_inv o := by rcases o with (⟨x, h⟩ | ⟨x, h⟩) <;> [simp [hs _ h]; simp [ht _ h]]
