isDirected_subset — Mathlib

English

The Finset inclusion order is directed; i.e., for any two Finsets s,t there exists u with s ⊆ u and t ⊆ u.

Русский

Порядок включения Finset направлен; то есть для любых s,t существует u, такой что s ⊆ u и t ⊆ u.

LaTeX

$$$$ \forall s,t: Finset α, \ exists\ u: Finset α \text{ with } s \subseteq u \land t \subseteq u. $$$$

Lean4

instance isDirected_subset : IsDirected (Finset α) (· ⊆ ·) :=
  isDirected_le

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