dual_isBase_iff' — Mathlib

English

For any B, M✶.IsBase B iff M.IsBase (M.E \ B) and B ⊆ M.E.

Русский

Для любого B верно: B является базисом дуала M✶ тогда и только тогда, когда M.IsBase (M.E \ B) и B ⊆ M.E.

LaTeX

$$M✶.IsBase B \iff (M.IsBase (M.E \ B) ∧ B ⊆ M.E)$$

Lean4

theorem dual_isBase_iff' : M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E :=
  (em (B ⊆ M.E)).elim (fun h ↦ by rw [dual_isBase_iff, and_iff_left h])
    (fun h ↦ iff_of_false (h ∘ (fun h' ↦ h'.subset_ground)) (h ∘ And.right))

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