disjointSum_isBase_iff — Mathlib

English

A base B of M.disjointSum N h corresponds to bases on the intersections with the component grounds and subset relations with respect to M.E ∪ N.E.

Русский

Базис B раздельной суммы соответствует базисам на пересечениях с основаниями компонентов и соотношениям подмножеств относительно M.E ∪ N.E.

LaTeX

$$$$ (M.disjointSum N h).IsBase B \iff M.IsBase (B \cap M.E) \land N.IsBase (B \cap N.E) \land B \subseteq M.E \cup N.E. $$$$

Lean4

@[simp]
theorem disjointSum_isBase_iff {h B} :
    (M.disjointSum N h).IsBase B ↔ M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E := by
  simp [disjointSum, and_assoc]

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