mem_iff — Mathlib

English

For any s ⊆ Set β and x ∈ β, x ∈ l s iff ∀ S ∈ α with s ⊆ S, x ∈ S.

Русский

Для любого s ⊆ Set β и x ∈ β верно: x ∈ l s тогда и только тогда, когда для всех S ∈ α, если s ⊆ S, то x ∈ S.

LaTeX

$$$x \in l(s) \iff \forall S:\alpha,\ s \subseteq S \Rightarrow x \in S$$$

Lean4

theorem mem_iff (s : Set β) (x : β) : x ∈ l s ↔ ∀ S : α, s ⊆ S → x ∈ S :=
  by
  simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← l.le_iff_subset]
  exact ⟨fun h S => h.trans, fun h => h _ le_rfl⟩

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