sup_eq_top_iff — Mathlib

English

p ⊔ p' = ⊤ if and only if every vector m ∈ M can be written as m = u + v with u ∈ p and v ∈ p'.

Русский

p ⊔ p' = ⊤ тогда и только тогда, когда любой вектор m можно разложить как m = u + v с u ∈ p, v ∈ p'.

LaTeX

$$$$ p \\sqcup p' = \\top \\iff \\forall m \\in M, \\exists u \\in p, \\exists v \\in p', m = u+v. $$$$

Lean4

theorem sup_eq_top_iff : p ⊔ p' = ⊤ ↔ ∀ m : M, ∃ u ∈ p, ∃ v ∈ p', m = u + v :=
  by
  rw [eq_top_iff']
  refine forall_congr' fun m ↦ ?_
  rw [mem_sup]
  tauto

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