le_basis_iff — Mathlib

English

If l and l' have HasBasis with p s and p' s', then l ≤ l' iff ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i'.

Русский

Если л и л' имеют базисы, то л ≤ л' эквивалентно: для каждого i' существует i, такой что p i ∧ s i ⊆ s' i'.

LaTeX

$$le_basis_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : l ≤ l' ↔ ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i'$$

Lean4

theorem le_basis_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : l ≤ l' ↔ ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i' :=
  by simp only [hl'.ge_iff, hl.mem_iff]

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