mulEnergy_pos_iff — Mathlib

English

0 < E_m[s,t] iff s and t are nonempty.

Русский

0 < E_m[s,t] эквивалентно тому, что s и t непусты.

LaTeX

$$$0 < E_m[s,t] \\iff s.Nonempty \\land t.Nonempty$$$

Lean4

@[to_additive (attr := simp)]
theorem mulEnergy_pos_iff : 0 < Eₘ[s, t] ↔ s.Nonempty ∧ t.Nonempty
    where
  mp
    h :=
    of_not_not fun H => by
      simp_rw [not_and_or, not_nonempty_iff_eq_empty] at H
      obtain rfl | rfl := H <;> simp at h
  mpr h := mulEnergy_pos h.1 h.2

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