English
For f: α → ENNReal that is almost everywhere measurable and a finite integral, the real-valued density μ.withDensityᵥ f equals the signed measure of μ.withDensity f via the real part.
Русский
Для f: α → ENNReal измеримой почти всюду и имеющей конечный интеграл, плотность μ.withDensityᵥ f равна знаковой мере μ.withDensity f через вещественную часть.
LaTeX
$$$(\mu.withDensityᵥ f).toReal = (\mu.withDensity f).toSignedMeasure$$
Lean4
/-- The first-order sentence corresponding to each field axiom -/
@[simp]
def toSentence : FieldAxiom → Language.ring.Sentence
| .addAssoc => ∀'∀'∀'(((&0 + &1) + &2) =' (&0 + (&1 + &2)))
| .zeroAdd => ∀'(((0 : Language.ring.Term _) + &0) =' &0)
| .negAddCancel => ∀'∀'((-&0 + &0) =' 0)
| .mulAssoc => ∀'∀'∀'(((&0 * &1) * &2) =' (&0 * (&1 * &2)))
| .mulComm => ∀'∀'((&0 * &1) =' (&1 * &0))
| .oneMul => ∀'(((1 : Language.ring.Term _) * &0) =' &0)
| .existsInv => ∀'(∼(&0 =' 0) ⟹ ∃'((&0 * &1) =' 1))
| .leftDistrib => ∀'∀'∀'((&0 * (&1 + &2)) =' ((&0 * &1) + (&0 * &2)))
| .existsPairNE => ∃'∃'(∼(&0 =' &1))
