instSubtractionCommMonoid — Mathlib

English

For any directed set c of LinearPMap, the domain of their supremum is the supremum of their domains.

Русский

Для направленного множества частичных линейных отображений их супремум имеет область определения, равную верхушке объединения их областей определения.

LaTeX

$$$$ \\operatorname{dom}(\\mathrm{LinearPMap}.sSup(c)) = \\operatorname{dom}(\\mathrm{domain})''c. $$$$

Lean4

instance instSubtractionCommMonoid : SubtractionCommMonoid (E →ₗ.[R] F)
    where
  add_comm := add_comm
  sub_eq_add_neg f
    g := by
    ext x _ h
    · rfl
    simp [sub_apply, add_apply, neg_apply, ← sub_eq_add_neg]
  neg_neg := neg_neg
  neg_add_rev f
    g := by
    ext x _ h
    · simp [add_domain, neg_domain, And.comm]
    simp [add_apply, neg_apply, ← sub_eq_add_neg]
  neg_eq_of_add f g
    h' := by
    ext x hf hg
    · have : (0 : E →ₗ.[R] F).domain = ⊤ := zero_domain
      simp only [← h', add_domain, inf_eq_top_iff] at this
      rw [neg_domain, this.1, this.2]
    simp only [neg_domain, neg_apply, neg_eq_iff_add_eq_zero]
    rw [ext_iff] at h'
    rcases h' with ⟨hdom, h'⟩
    rw [zero_domain] at hdom
    simp only [hdom, zero_domain, mem_top, zero_apply, forall_true_left] at h'
    apply h'
  zsmul := zsmulRec

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