English
If c ≠ 0, equal indicatorConstLp for two measurable sets s,t with finite μ-measures implies s =ᵐ μ t.
Русский
Если c ≠ 0 и двух индикаторов равны, тогда множества равны μ-эквивалентно.
LaTeX
$$indicatorConstLp(p, hs, hμs, c) = indicatorConstLp(p, ht, hμt, c) ⇔ s =ᵐ_{μ} t (for c ≠ 0).$$
Lean4
theorem indicatorConstLp_inj {s t : Set α} (hs : MeasurableSet s) (hsμ : μ s ≠ ∞) (ht : MeasurableSet t) (htμ : μ t ≠ ∞)
{c : E} (hc : c ≠ 0) : indicatorConstLp p hs hsμ c = indicatorConstLp p ht htμ c ↔ s =ᵐ[μ] t := by
simp_rw [← indicator_const_eventuallyEq hc, indicatorConstLp, MemLp.toLp_eq_toLp_iff]