star_iff — Mathlib

English

The star operation preserves membership in Memℓp: Memℓp (star f) p if and only if Memℓp f p.

Русский

Операция star сохраняет принадлежность к Memℓp: Memℓp (star f) p эквивалентно Memℓp f p.

LaTeX

$$$Mem\\ell p (star f) p \\iff Mem\\ell p f p$$$

Lean4

@[simp]
theorem _root_.Memℓp.star_iff {f : ∀ i, E i} : Memℓp (star f) p ↔ Memℓp f p :=
  ⟨fun h => star_star f ▸ Memℓp.star_mem h, Memℓp.star_mem⟩

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