English
For a submodule g of E × F and a point x = (x.fst, x.snd) ∈ F × E, x belongs to the adjoint g.adjoint iff for every a ∈ E and b ∈ F, (a, b) ∈ g implies ⟪b, x.fst⟫ − ⟪a, x.snd⟫ = 0.
Русский
Для подмодуля g ⊆ E × F и точки x = (x.fst, x.snd) в F × E принадлежность x к сопряжённости g.adjoint эквивалентна тому, что для всех a ∈ E и b ∈ F, если (a, b) ∈ g, то ⟪b, x.fst⟫ − ⟪a, x.snd⟫ = 0.
LaTeX
$$$x \\in g^{\\perp} \\iff \\forall a,b,\\ (a,b) \\in g \\Rightarrow \\langle b, x_{\\text{fst}} \\rangle - \\langle a, x_{\\text{snd}} \\rangle = 0$$$
Lean4
@[simp]
theorem mem_adjoint_iff (g : Submodule 𝕜 (E × F)) (x : F × E) :
x ∈ g.adjoint ↔ ∀ a b, (a, b) ∈ g → inner 𝕜 b x.fst - inner 𝕜 a x.snd = 0 :=
by
simp only [Submodule.adjoint, mem_map, mem_orthogonal, LinearEquiv.trans_apply, LinearEquiv.skewSwap_symm_apply,
WithLp.linearEquiv_symm_apply, Prod.exists, WithLp.prod_inner_apply, WithLp.ofLp_fst, WithLp.ofLp_snd,
forall_exists_index, and_imp, WithLp.linearEquiv_apply]
constructor
· rintro ⟨y, h1, h2⟩ a b hab
rw [← h2, WithLp.ofLp_fst, WithLp.ofLp_snd]
specialize h1 (b, -a) a b hab rfl
dsimp at h1
simp only [inner_neg_left, ← sub_eq_add_neg] at h1
exact h1
· intro h
refine ⟨x, ?_, rfl⟩
intro u a b hab hu
simp [← hu, ← sub_eq_add_neg, h a b hab]
