English
A germ P is constant with respect to l if there exists a β such that P is represented by a function whose values are constantly b on a l-almost everywhere set.
Русский
Жермен постоянен по отношению к l, если существует b∈β, такая репрезентация функции, что она равно b почти всюду по l.
LaTeX
$$$\mathrm{IsConstant}(P) := P.liftOn(\\f => \exists b:\\beta, f =^l (\\lambda _ => b)) <| ...$$$
Lean4
/-- A germ `P` of functions `α → β` is constant w.r.t. `l`. -/
def IsConstant {l : Filter α} (P : Germ l β) : Prop :=
P.liftOn (fun f ↦ ∃ b : β, f =ᶠ[l] (fun _ ↦ b)) <|
by
suffices ∀ f g : α → β, ∀ b : β, f =ᶠ[l] g → (f =ᶠ[l] fun _ ↦ b) → (g =ᶠ[l] fun _ ↦ b) from fun f g h ↦
propext ⟨fun ⟨b, hb⟩ ↦ ⟨b, this f g b h hb⟩, fun ⟨b, hb⟩ ↦ ⟨b, h.trans hb⟩⟩
exact fun f g b hfg hf ↦ (hfg.symm).trans hf
