English
Let s be a preirreducible subset of X and f: X → Y a map which is continuous on s. Then the image f[s] is preirreducible in Y.
Русский
Пусть s — преднеразложимое подмножество X, и отображение f: X → Y непрерывно на s. Тогда образ f[s] является преднеразложимым в Y.
LaTeX
$$$\mathrm{IsPreirreducible}(s) \;\rightarrow\; (f:X\to Y) \;\rightarrow\; \mathrm{ContinuousOn}(f,s) \;\rightarrow\; \mathrm{IsPreirreducible}(f''s)$$$
Lean4
theorem image (H : IsPreirreducible s) (f : X → Y) (hf : ContinuousOn f s) : IsPreirreducible (f '' s) :=
by
rintro u v hu hv ⟨_, ⟨⟨x, hx, rfl⟩, hxu⟩⟩ ⟨_, ⟨⟨y, hy, rfl⟩, hyv⟩⟩
rw [← mem_preimage] at hxu hyv
rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩
have := H u' v' hu' hv'
rw [inter_comm s u', ← u'_eq] at this
rw [inter_comm s v', ← v'_eq] at this
rcases this ⟨x, hxu, hx⟩ ⟨y, hyv, hy⟩ with ⟨x, hxs, hxu', hxv'⟩
refine ⟨f x, mem_image_of_mem f hxs, ?_, ?_⟩
all_goals
rw [← mem_preimage]
apply mem_of_mem_inter_left
show x ∈ _ ∩ s
simp [*]
