mem_comap_prodMk — Mathlib

English

For x ∈ α and s ⊆ β with F a filter on α×β, membership in comap (Prod.mk x) F is equivalent to membership of a certain subset of α×β in F.

Русский

Для x ∈ α и s ⊆ β при F — фильтре на α×β эквивалентно членство в F множества {p ∈ α×β | p.fst = x → p.snd ∈ s}.

LaTeX

$$s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.fst = x → p.snd ∈ s} ∈ F$$

Lean4

/-- RHS form is used, e.g., in the definition of `UniformSpace`. -/
theorem mem_comap_prodMk {x : α} {s : Set β} {F : Filter (α × β)} :
    s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.fst = x → p.snd ∈ s} ∈ F := by
  simp_rw [mem_comap', Prod.ext_iff, and_imp, @forall_swap β (_ = _), forall_eq, eq_comm]

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