generateFrom_insert_of_generateOpen

English

If t is generated open by s, then generating from insert t s equals generating from s.

Русский

Если t есть открытым при генерации из s, то generateFrom(insert t s) = generateFrom(s).

LaTeX

$$∀ {α : Type*} {s : Set (Set α)} {t : Set α}, (ht : GenerateOpen s t) → generateFrom (insert t s) = generateFrom s$$

Lean4

theorem generateFrom_insert_of_generateOpen {α : Type*} {s : Set (Set α)} {t : Set α} (ht : GenerateOpen s t) :
    generateFrom (insert t s) = generateFrom s :=
  by
  refine le_antisymm (generateFrom_anti <| subset_insert t s) (le_generateFrom ?_)
  rintro t (rfl | h)
  · exact ht
  · exact isOpen_generateFrom_of_mem h

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