mono

Mathlib.Topology.Coherent

URI: https://scilib.ai/kg/mathlib#Topology.IsCoherentWith.mono

English

If S is coherent with S and S is a subset of T, then T is coherent.

Русский

Если S когерентно, а S ⊆ T, то T когерентно.

LaTeX

$$$ \\text{IsCoherentWith } S \\to (S \\subseteq T) \\to \\text{IsCoherentWith } T $$$

Lean4

protected theorem mono {T} (hS : IsCoherentWith S) (hT : S ⊆ T) : IsCoherentWith T :=
  hS.enlarge fun s hs ↦ ⟨s, hT hs, Subset.rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru