English
For any set s and p(i), the big supremum of comaps along subtypes equals top.
Русский
Для множества s и подмодулей p(i) верхняя грань объединения комап совпадает с верхом.
LaTeX
$$$$ ⨆ i ∈ s, (p(i)).comap ((⨆ i ∈ s, p(i)).subtype) = ⊤ $$$$
Lean4
/-- If a bilinear map takes values in a submodule along two sets, then the same is true along
the span of these sets. -/
theorem _root_.LinearMap.BilinMap.apply_apply_mem_of_mem_span {R M N P : Type*} [CommSemiring R] [AddCommMonoid M]
[AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (P' : Submodule R P) (s : Set M)
(t : Set N) (B : M →ₗ[R] N →ₗ[R] P) (hB : ∀ x ∈ s, ∀ y ∈ t, B x y ∈ P') (x : M) (y : N) (hx : x ∈ span R s)
(hy : y ∈ span R t) : B x y ∈ P' := by
induction hx, hy using span_induction₂ with
| mem_mem u v hu hv => exact hB u hu v hv
| zero_left v hv => simp
| zero_right u hu => simp
| add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
| add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
| smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
| smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
