polar_subMulAction — Mathlib

English

Same as earlier: polar equals zero on the submul action domain.

Русский

То же самое: поляр равна нулю на области действия подскаляра.

LaTeX

$$$B.polar(m) = \{ y : \forall x \in m, B(x,y)=0\}$$$

Lean4

theorem polar_subMulAction {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) :
    B.polar m = {y | ∀ x ∈ m, B x y = 0} := by
  ext y
  constructor
  · intro hy x hx
    obtain ⟨r, hr⟩ := NormedField.exists_lt_norm 𝕜 ‖B x y‖⁻¹
    contrapose! hr
    rw [← one_div, le_div_iff₀ (norm_pos_iff.2 hr)]
    simpa using hy _ (SMulMemClass.smul_mem r hx)
  · intro h x hx
    simp [h x hx]

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