English
Given a fixed equivalence e0 : s ≃ t, the set of all e : α ≃ β that extend e0 on s is bijective to the set of bijections between the complements sᶜ and tᶜ.
Русский
Заданная существующая эквивалентность e0 : s ≃ t, множество биекций e : α ≃ β, которые согласованы с e0 на s, взаимно однозначно эквивалентно множеству биекций между комплементами sᶜ и tᶜ.
LaTeX
$${ e : α ≃ β // ∀ x : s, e x = e0 x } \;\simeq\; (s^c \ ≃ t^c)$$
Lean4
/-- Given an equivalence `e₀` between sets `s : Set α` and `t : Set β`, the set of equivalences
`e : α ≃ β` such that `e ↑x = ↑(e₀ x)` for each `x : s` is equivalent to the set of equivalences
between `sᶜ` and `tᶜ`. -/
protected def compl {α : Type u} {β : Type v} {s : Set α} {t : Set β} [DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)]
(e₀ : s ≃ t) : { e : α ≃ β // ∀ x : s, e x = e₀ x } ≃ ((sᶜ : Set α) ≃ (tᶜ : Set β))
where
toFun
e :=
subtypeEquiv e fun _ =>
not_congr <|
Iff.symm <|
MapsTo.mem_iff (mapsTo_iff_exists_map_subtype.2 ⟨e₀, e.2⟩)
(SurjOn.mapsTo_compl (surjOn_iff_exists_map_subtype.2 ⟨t, e₀, Subset.refl t, e₀.surjective, e.2⟩)
e.1.injective)
invFun
e₁ :=
Subtype.mk
(calc
α ≃ s ⊕ (sᶜ : Set α) := (Set.sumCompl s).symm
_ ≃ t ⊕ (tᶜ : Set β) := (e₀.sumCongr e₁)
_ ≃ β := Set.sumCompl t)
fun x => by
simp only [Sum.map_inl, trans_apply, sumCongr_apply, Set.sumCompl_apply_inl, Set.sumCompl_symm_apply, Trans.trans]
left_inv
e := by
ext x
by_cases hx : x ∈ s
·
simp only [Set.sumCompl_symm_apply_of_mem hx, ← e.prop ⟨x, hx⟩, Sum.map_inl, sumCongr_apply, trans_apply,
Set.sumCompl_apply_inl, Trans.trans]
·
simp only [Set.sumCompl_symm_apply_of_notMem hx, Sum.map_inr, subtypeEquiv_apply, Set.sumCompl_apply_inr,
trans_apply, sumCongr_apply, Trans.trans]
right_inv
e :=
Equiv.ext fun x => by
simp only [Sum.map_inr, subtypeEquiv_apply, Set.sumCompl_apply_inr, Function.comp_apply, sumCongr_apply,
Equiv.coe_trans, Subtype.coe_eta, Trans.trans, Set.sumCompl_symm_apply_compl]
