A case study of transporting Urysohn's lemma from topology via open sets into topology via neighborhoods

DOI10.2478/FORMA-2020-0020zbMATH Open1543.68416MaRDI QIDQ6592310

Roland Coghetto

Publication date: 26 August 2024

Published in: Formalized Mathematics (Search for Journal in Brave)

zbMATH Keywords

filtertransfer principletransport of structuretopology via neighborhoods

Mathematics Subject Classification ID

Topological spaces and generalizations (closure spaces, etc.) (54A05) Mechanization of proofs and logical operations (03B35) Higher separation axioms (completely regular, normal, perfectly or collectionwise normal, etc.) (54D15) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Topology from neighbourhoods
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Topology. Exercises and solved problems
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Mizar: State-of-the-art and Beyond
• Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
• Changing Data Representation within the Coq System
• Theorem Proving in Higher Order Logics
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.

This page was built for publication: A case study of transporting Urysohn's lemma from topology via open sets into topology via neighborhoods

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6592310)