le_flip_dualSubmodule — Mathlib

English

There is a natural pairing between B.dualSubmodule N and N given by (x,y) ↦ B(x,y). This pairing is used to define a bilinear map B.dualSubmoduleToDual.

Русский

Существует естественная парная связь между B.dualSubmodule N и N, заданная парой (x,y) ↦ B(x,y). Эта связь задаёт билинейную карту B.dualSubmoduleToDual.

LaTeX

$$$$ \text{pairing: } (x,y) \mapsto B(x,y) \quad \text{with } x \in B.dualSubmodule(N),\; y \in N. $$$$

Lean4

theorem le_flip_dualSubmodule {N₁ N₂ : Submodule R M} : N₁ ≤ B.flip.dualSubmodule N₂ ↔ N₂ ≤ B.dualSubmodule N₁ :=
  by
  change (∀ (x : M), x ∈ N₁ → _) ↔ ∀ (x : M), x ∈ N₂ → _
  simp only [mem_dualSubmodule, Submodule.mem_one, flip_apply]
  exact forall₂_swap

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