inter_mem_iff — Mathlib

English

s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f.

Русский

Пересечение двух множеств принадлежит фильтру тогда и только тогда оба множества принадлежат фильтру.

LaTeX

$$$s \cap t \in f \iff s \in f \wedge t \in f$$$

Lean4

@[simp]
theorem inter_mem_iff {s t : Set α} : s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f :=
  ⟨fun h => ⟨mem_of_superset h inter_subset_left, mem_of_superset h inter_subset_right⟩, and_imp.2 inter_mem⟩

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