mono — Mathlib

English

Monotonicity: If S generates Boolean generators, then every subset T ⊆ S also generates Boolean generators.

Русский

Монотонность: если S порождает булевы генераторы, то и любая подмножество T ⊆ S порождает булевы генераторы.

LaTeX

$$$ \text{BooleanGenerators}(S) \rightarrow (T \subseteq S) \rightarrow \text{BooleanGenerators}(T) $$$

Lean4

theorem mono (hS : BooleanGenerators S) {T : Set α} (hTS : T ⊆ S) : BooleanGenerators T
    where
  isAtom I hI := hS.isAtom I (hTS hI)
  finitelyAtomistic := fun s a hs ↦ hS.finitelyAtomistic s a (le_trans hs hTS)

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