forall_mem_mem — Mathlib

English

If h is a HasBasis l p s, then for every x, (for all t ∈ l, x ∈ t) is equivalent to (for all i, p i → x ∈ s i).

Русский

Если h — HasBasis l p s, то для каждого x верно: (для всех t ∈ l, x ∈ t) эквивалентно (для всех i, p i → x ∈ s i).

LaTeX

$$$ \forall x,\ (\forall t \in l, x \in t) \iff \forall i, p i \to x \in s i $$$

Lean4

theorem forall_mem_mem (h : HasBasis l p s) {x : α} : (∀ t ∈ l, x ∈ t) ↔ ∀ i, p i → x ∈ s i :=
  by
  simp only [h.mem_iff, exists_imp, and_imp]
  exact ⟨fun h i hi => h (s i) i hi Subset.rfl, fun h t i hi ht => ht (h i hi)⟩

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