English
The set {u in U | meromorphicOrderAt f u = ⊤} is a clopen subset of U.
Русский
Множество {u ∈ U | meromorphicOrderAt f u = ⊤} является открытым и его дополнение тоже открыто в U.
LaTeX
$$$\\mathrm{IsClopen}\\{u \\in U \\mid \\operatorname{meromorphicOrderAt} f u = \\top\\}$$$
Lean4
/-- The set where a meromorphic function has infinite order is clopen in its domain of meromorphy.
-/
theorem isClopen_setOf_meromorphicOrderAt_eq_top (hf : MeromorphicOn f U) :
IsClopen {u : U | meromorphicOrderAt f u = ⊤} := by
constructor
· rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]
intro z hz
rcases (hf z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h
· -- Case: f is locally zero in a punctured neighborhood of z
rw [← meromorphicOrderAt_eq_top_iff] at h
tauto
· -- Case: f is locally nonzero in a punctured neighborhood of z
obtain ⟨t', h₁t', h₂t', h₃t'⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h)
use Subtype.val ⁻¹' t'
constructor
· intro w hw
simp only [mem_compl_iff, mem_setOf_eq]
by_cases h₁w : w = z
· rwa [h₁w]
· rw [meromorphicOrderAt_eq_top_iff, not_eventually]
apply Filter.Eventually.frequently
rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
use t' \ { z.1 }, fun y h₁y h₂y ↦ h₁t' y h₁y.1 h₁y.2, h₂t'.sdiff isClosed_singleton, hw,
mem_singleton_iff.not.2 (Subtype.coe_ne_coe.mpr h₁w)
· exact ⟨isOpen_induced h₂t', h₃t'⟩
· apply isOpen_iff_forall_mem_open.mpr
intro z hz
conv =>
arg 1; intro; left; right; arg 1; intro
rw [meromorphicOrderAt_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
simp only [mem_setOf_eq] at hz
rw [meromorphicOrderAt_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at hz
obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
use Subtype.val ⁻¹' t'
simp only [mem_compl_iff, mem_singleton_iff, isOpen_induced h₂t', mem_preimage, h₃t', and_self, and_true]
intro w hw
simp only [mem_setOf_eq]
-- Trivial case: w = z
by_cases h₁w : w = z
· rw [h₁w]
tauto
-- Nontrivial case: w ≠ z
use t' \ { z.1 }, fun y h₁y _ ↦ h₁t' y (mem_of_mem_diff h₁y) (mem_of_mem_inter_right h₁y)
constructor
· exact h₂t'.sdiff isClosed_singleton
· apply (mem_diff w).1
exact ⟨hw, mem_singleton_iff.not.1 (Subtype.coe_ne_coe.2 h₁w)⟩
