%
%
% Purpose: results to get rid of is_finite TCCs
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
%
finite_sets_below_extra[N: nat]: THEORY
BEGIN
IMPORTING finite_sets@finite_sets_below[N]
below_is_finite_type: LEMMA is_finite_type[below(N)]
set_below_is_finite: JUDGEMENT set[below(N)] SUBTYPE_OF finite_set[below(N)]
END finite_sets_below_extra
| Messung V0.5 in Prozent |
|---|
| | | |
[Konzepte0.13Was zu einem Entwurf gehörtWie die Entwicklung von Software durchgeführt wird2026-09-29]