English
Let I be an index set, C ⊆ (I → Bool) a family of booleans, and J : I → Prop a decidable predicate. Then the map iso_map C J is a bijection between the two natural sets determined by C and J (as constructed in the Nobeling proof).
Русский
Пусть I — множество индексов, C ⊆ (I → Bool) задаёт семейство булевых функций, и J : I → Prop — декидируемый предикат. Тогда отображение iso_map C J является биекцией между двумя естественными множестами, определёнными C и J (как это устроено в доказательстве Нобелей).
LaTeX
$$$\operatorname{Bijective}(\mathrm{iso\_map}(C,J))$$$
Lean4
theorem iso_map_bijective : Function.Bijective (iso_map C J) :=
by
refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩
· ext i
rw [Subtype.ext_iff] at h
by_cases hi : J i
· exact congr_fun h ⟨i, hi⟩
· rcases a with ⟨_, c, hc, rfl⟩
rcases b with ⟨_, d, hd, rfl⟩
simp only [Proj, if_neg hi]
· refine ⟨⟨fun i ↦ if hi : J i then a.val ⟨i, hi⟩ else false, ?_⟩, ?_⟩
· rcases a with ⟨_, y, hy, rfl⟩
exact ⟨y, hy, rfl⟩
· ext i
exact dif_pos i.prop
