mem_inf_iff_superset — Mathlib

English

The infimum membership is equivalent to the existence of witnesses t1 ∈ f and t2 ∈ g with t1 ∩ t2 ⊆ s.

Русский

Принадлежность к инфимууму эквивалентна существованию свидетелей t1 ∈ f и t2 ∈ g с t1 ∩ t2 ⊆ s.

LaTeX

$$$s \\in f \\sqcap g \\iff \\exists t_1 \\in f, \\exists t_2 \\in g, t_1 \\cap t_2 \\subseteq s$$$

Lean4

theorem mem_inf_iff_superset {f g : Filter α} {s : Set α} : s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ∩ t₂ ⊆ s :=
  ⟨fun ⟨t₁, h₁, t₂, h₂, Eq⟩ => ⟨t₁, h₁, t₂, h₂, Eq ▸ Subset.rfl⟩, fun ⟨_, h₁, _, h₂, sub⟩ => mem_inf_of_inter h₁ h₂ sub⟩

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