English
If a UniqueHom instance exists, then cfc_nHom ha equals cfc_nHom_of_cfcHom R ha.
Русский
При наличии единичного гомоморфа равенство cfc_nHom ha = cfc_nHom_of_cfcHom R ha выполняется.
LaTeX
$$$$ cfc\\!_nHom ha = cfc\\!_nHom\\_of\\_cfcHom R ha $$$$
Lean4
theorem cfcₙ_neg : cfcₙ (fun x ↦ -(f x)) a = -(cfcₙ f a) :=
by
by_cases h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
· obtain ⟨ha, hf, h0⟩ := h
rw [cfcₙ_apply f a, ← map_neg, cfcₙ_apply ..]
congr
· simp only [not_and_or] at h
obtain (ha | hf | h0) := h
· simp [cfcₙ_apply_of_not_predicate a ha]
· rw [cfcₙ_apply_of_not_continuousOn a hf, cfcₙ_apply_of_not_continuousOn, neg_zero]
exact fun hf_neg ↦ hf <| by simpa using hf_neg.neg
· rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, neg_zero]
exact (h0 <| neg_eq_zero.mp ·)
