exchange — 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 such that 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 \in B_2 \setminus B_1, M.IsBase (insert y (B_1 \ \{ e \})) $$$$

Lean4

theorem exchange {e : α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) (hx : e ∈ B₁ \ B₂) :
    ∃ y ∈ B₂ \ B₁, M.IsBase (insert y (B₁ \ { e })) :=
  M.isBase_exchange B₁ B₂ hB₁ hB₂ _ hx

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