generate_le — Mathlib

English

The Dynkin-system generated by a collection s is contained in a Dynkin system d whenever every element of s is in d.

Русский

Порожденная динкинсовая система порожденной коллекции s содержится в d, если каждый элемент s принадлежит d.

LaTeX

$$$ \forall d:\text{DynkinSystem}(\alpha), \forall s:\Set(\Set(\alpha)), \Big( \forall t\in s, \ t\in d \Big) \Rightarrow \ generate(s) \le d. $$$

Lean4

theorem generate_le {s : Set (Set α)} (h : ∀ t ∈ s, d.Has t) : generate s ≤ d := fun _ ht =>
  ht.recOn h d.has_empty (fun {_} _ h => d.has_compl h) fun {_} hd _ hf => d.has_iUnion hd hf

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