union_mem_iff — Mathlib

English

s ∪ t ∈ f if and only if s ∈ f or t ∈ f.

Русский

Объединение s и t принадлежит f тогда и только тогда, когда s принадлежит f или t принадлежит f.

LaTeX

$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {s t \\\\subseteq \\\\alpha}, s \\\\cup t \in f \\\\Leftrightarrow s \\\\in f \\\\lor t \\\\in f$$$

Lean4

@[simp]
theorem union_mem_iff : s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f := by
  simp only [← mem_coe, ← le_principal_iff, ← sup_principal, le_sup_iff]

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