exchange_mem — Mathlib

English

If e ∈ B1 and e ∉ B2, there exists y ∈ B2 \ B1 with M.IsBase (insert y (B1 \ { e })).

Русский

Если e ∈ B1 и e ∉ B2, существует y ∈ B2 \ B1 такой, что M.IsBase (insert y (B1 \ { e })).

LaTeX

$$$$ \forall {e} (hB_1 : M.IsBase B_1) (hB_2 : M.IsBase B_2) (hxB_1 : e \in B_1) (hxB_2 : e \notin B_2), \exists y, (y \in B_2 \land y \notin B_1) \land M.IsBase (insert y (B_1 \ { e })) $$$$

Lean4

theorem exchange_mem {e : α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) (hxB₁ : e ∈ B₁) (hxB₂ : e ∉ B₂) :
    ∃ y, (y ∈ B₂ ∧ y ∉ B₁) ∧ M.IsBase (insert y (B₁ \ { e })) := by simpa using hB₁.exchange hB₂ ⟨hxB₁, hxB₂⟩

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