generatePiSystem_mono — Mathlib

English

If S ⊆ T then generatePiSystem(S) ⊆ generatePiSystem(T).

Русский

Если S ⊆ T, то generatePiSystem(S) ⊆ generatePiSystem(T).

LaTeX

$$$$ S \subseteq T \Rightarrow \mathrm{generatePiSystem}(S) \subseteq \mathrm{generatePiSystem}(T) $$$$

Lean4

theorem generatePiSystem_mono {S T : Set (Set α)} (hST : S ⊆ T) : generatePiSystem S ⊆ generatePiSystem T := fun t ht =>
  by
  induction ht with
  | base h_s => exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)
  | inter _ _ h_nonempty h_s h_u => exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty

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