indicatorConstLp_inj — Mathlib

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]

Похожие утверждения