mem_inf — Mathlib

English

Membership in the infimum of Pretopologies is equivalent to membership in all components.

Русский

Членство в инфимуме препотопологий эквивалентно членству во всех компонентах.

LaTeX

$$$S \\in (t_1 \\inf t_2) X \\iff S \\in t_1 X \\land S \\in t_2 X$$$

Lean4

theorem mem_inf (t₁ t₂ : Pretopology C) {X : C} (S : Presieve X) : S ∈ (t₁ ⊓ t₂) X ↔ S ∈ t₁ X ∧ S ∈ t₂ X :=
  Iff.rfl

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